theorem :: VECTSP12:9

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