\left(V_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) \land \left(V_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) \land \ldots \land \left(V_{n} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right)\land \left(W_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) \land \left(W_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) \land \ldots \land \left(W_{n} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right)