let V be Z_Module; :: thesis: for W being Subspace of V
for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds
W is free

let W be Subspace of V; :: thesis: for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds
W is free

let W1, W2 be free Subspace of V; :: thesis: ( W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 implies W is free )
assume A1: ( W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 ) ; :: thesis: W is free
reconsider Ws = W1 + W2 as free Subspace of V by ;
consider I being Subset of Ws such that
a3: I is base by VECTSP_7:def 4;
A3: ( I is linearly-independent & Ws = Lin I ) by ;
reconsider IV = I as linearly-independent Subset of V by ;
reconsider IW = IV as linearly-independent Subset of W by ;
ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = Lin IV by
.= Lin IW by ZMODUL03:20 ;
then IW is base by VECTSP_7:def 3;
hence W is free by VECTSP_7:def 4; :: thesis: verum