for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being Basis of W1
for B2 being Basis of W2 holds B1 \/ B2 is Basis of (W1 + W2)