let V be Z_Module; :: thesis: for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V holds
W1 + W2 is free
let W1, W2 be free Subspace of V; :: thesis: ( W1 /\ W2 = (0). V implies W1 + W2 is free )
assume P1: W1 /\ W2 = (0). V ; :: thesis: W1 + W2 is free
reconsider W = W1 + W2 as strict Subspace of V ;
reconsider WW1 = W1 as Subspace of W by ZMODUL01:97;
reconsider WW2 = W2 as Subspace of W by ZMODUL01:97;
A2: WW1 /\ WW2 is Subspace of V by ZMODUL01:42;
A3: WW1 + WW2 is Subspace of V by ZMODUL01:42;
for x being object holds
( x in WW1 /\ WW2 iff x in (0). V )

proof

let x be object ; :: thesis: ( x in WW1 /\ WW2 iff x in (0). V )

hereby :: thesis: ( x in (0). V implies x in WW1 /\ WW2 )

assume x in WW1 /\ WW2 ; :: thesis: x in (0). V
then ( x in WW1 & x in WW2 ) by VECTSP_5:3;
hence x in (0). V by P1, VECTSP_5:3; :: thesis: verum

end;

assume x in (0). V ; :: thesis: x in WW1 /\ WW2
then ( x in W1 & x in W2 ) by P1, VECTSP_5:3;
hence x in WW1 /\ WW2 by VECTSP_5:3; :: thesis: verum

end;

then for x being Vector of V holds
( x in WW1 /\ WW2 iff x in (0). V ) ;
then A4: WW1 /\ WW2 = (0). V by A2, VECTSP_4:30
.= (0). W by ZMODUL01:51 ;
for x being object holds
( x in W iff x in WW1 + WW2 )

proof

let x be object ; :: thesis: ( x in W iff x in WW1 + WW2 )

hereby :: thesis: ( x in WW1 + WW2 implies x in W )

assume x in W ; :: thesis: x in WW1 + WW2
then consider x1, x2 being Vector of V such that
B2: ( x1 in W1 & x2 in W2 & x = x1 + x2 ) by VECTSP_5:1;
x1 in W1 + W2 by B2, VECTSP_5:2;
then reconsider xx1 = x1 as Vector of W ;
x2 in W1 + W2 by B2, VECTSP_5:2;
then reconsider xx2 = x2 as Vector of W ;
x = xx1 + xx2 by B2, ZMODUL01:28;
hence x in WW1 + WW2 by B2, VECTSP_5:1; :: thesis: verum

end;

assume x in WW1 + WW2 ; :: thesis: x in W
then consider x1, x2 being Vector of W such that
B2: ( x1 in WW1 & x2 in WW2 & x = x1 + x2 ) by VECTSP_5:1;
thus x in W by B2; :: thesis: verum

end;

then for x being Vector of V holds
( x in W iff x in WW1 + WW2 ) ;
then W = WW1 + WW2 by A3, VECTSP_4:30;
hence W1 + W2 is free by A4, FRdsX, VECTSP_5:def 4; :: thesis: verum