theorem FRds2: :: ZMODUL04:28

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
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)