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 w1 being OrdBasis of W1
for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2