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

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