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 A1, ThDirectSum;
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 VECTSP_7:def 3, a3;
reconsider IV = I as linearly-independent Subset of V by A3, ZMODUL03:15;
reconsider IW = IV as linearly-independent Subset of W by A1, ZMODUL03:16;
ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = Lin IV by A1, A3, ZMODUL03:20
.= 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