theorem FRds1: :: ZMODUL04:27

for V being Z_Module
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds
I1 /\ I2 = {}