let V be Z_Module; :: thesis: for W being free Subspace of V
for I being Subset of V
for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
let W be free Subspace of V; :: thesis: for I being Subset of V
for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
let I be Subset of V; :: thesis: for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
let v be Vector of V; :: thesis: ( I is linearly-independent & Lin I = (Omega). W & v in I implies ( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V ) )
assume A1: ( I is linearly-independent & Lin I = (Omega). W & v in I ) ; :: thesis: ( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
A2: (I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A1, ZFMISC_1:40 ;
A3: I \ {v} is linearly-independent by A1, ZMODUL02:56, XBOOLE_1:36;
A4: not v is torsion by A1, ThLIV1;
(Lin (I \ {v})) /\ (Lin {v}) = (0). V

proof

assume (Lin (I \ {v})) /\ (Lin {v}) <> (0). V ; :: thesis: contradiction
then consider x being Vector of V such that
B2: ( x in (Lin (I \ {v})) /\ (Lin {v}) & x <> 0. V ) by ZMODUL04:24;
x in Lin (I \ {v}) by B2, ZMODUL01:94;
then consider lx1 being Linear_Combination of I \ {v} such that
B3: x = Sum lx1 by ZMODUL02:64;
B4: Carrier lx1 <> {} by B2, B3, ZMODUL02:23;
reconsider llx1 = lx1 as Linear_Combination of I by XBOOLE_1:36, ZMODUL02:10;
x in Lin {v} by B2, ZMODUL01:94;
then consider lx2 being Linear_Combination of {v} such that
B5: - x = Sum lx2 by ZMODUL01:38, ZMODUL02:64;
reconsider llx2 = lx2 as Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;
B6: Carrier lx1 c= I \ {v} by VECTSP_6:def 4;
Carrier lx2 c= {v} by VECTSP_6:def 4;
then Carrier lx1 misses Carrier lx2 by B6, XBOOLE_1:64, XBOOLE_1:79;
then (Carrier lx1) /\ (Carrier lx2) = {} by XBOOLE_0:def 7;
then B7: Carrier (llx1 + llx2) = (Carrier llx1) \/ (Carrier llx2) by ZMODUL04:25;
B8: (Sum llx1) + (Sum llx2) = 0. V by B3, B5, RLVECT_1:5;
reconsider llx = llx1 + llx2 as Linear_Combination of I by ZMODUL02:27;
Sum llx = 0. V by B8, ZMODUL02:52;
hence contradiction by A1, B4, B7; :: thesis: verum

end;

hence ( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V ) by A2, A3, A4, A1, ZMODUL02:72, ThnTV4; :: thesis: verum