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

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