let V be Z_Module; :: thesis: for W1, W2 being free Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is free
let W1, W2 be free Subspace of V; :: thesis: ( V is_the_direct_sum_of W1,W2 implies V is free )
assume A1: V is_the_direct_sum_of W1,W2 ; :: thesis: V is free
set I1 = the Basis of W1;
set I2 = the Basis of W2;
set I = the Basis of W1 \/ the Basis of W2;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then A3: the Basis of W1 is Subset of V by XBOOLE_1:1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then the Basis of W2 is Subset of V by XBOOLE_1:1;
then reconsider I = the Basis of W1 \/ the Basis of W2 as Subset of V by A3, XBOOLE_1:8;
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = Lin I by A1, FRds2;
then I is base by VECTSP_7:def 3, FRds3, A1;
hence V is free by VECTSP_7:def 4; :: thesis: verum