theorem Th2: :: MATRLIN2:2
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 linearly-independent Subset of W1
for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2)