for K being Field
for V1 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)