let V be finitely-generated torsion-free Z_Module; :: thesis: V is free
consider A being finite Subset of V such that
A2: Lin A = (Omega). V by ZMODUL03:def 4;
A3: Lin (A \ {(0. V)}) is free

proof

defpred S₁[ Nat] means for B being finite Subset of V st card (B \ {(0. V)}) = c₁ holds
Lin (B \ {(0. V)}) is free ;
B2: S₁[ 0 ]

proof

let B be finite Subset of V; :: thesis: ( card (B \ {(0. V)}) = 0 implies Lin (B \ {(0. V)}) is free )
assume C1: card (B \ {(0. V)}) = 0 ; :: thesis: Lin (B \ {(0. V)}) is free
B \ {(0. V)} = {} the carrier of V by C1;
hence Lin (B \ {(0. V)}) is free ; :: thesis: verum

end;

B3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume C1: S₁[n] ; :: thesis: S₁[n + 1]
let B be finite Subset of V; :: thesis: ( card (B \ {(0. V)}) = n + 1 implies Lin (B \ {(0. V)}) is free )
assume C2: card (B \ {(0. V)}) = n + 1 ; :: thesis: Lin (B \ {(0. V)}) is free
B \ {(0. V)} <> {} by C2;
then consider u being object such that
C3: u in B \ {(0. V)} by XBOOLE_0:7;
reconsider u = u as Vector of V by C3;
C4: card ((B \ {(0. V)}) \ {u}) = (card (B \ {(0. V)})) - (card {u}) by C3, ZFMISC_1:31, CARD_2:44
.= (n + 1) - 1 by C2, CARD_1:30
.= n ;
(B \ {(0. V)}) \ {u} = B \ ({(0. V)} \/ {u}) by XBOOLE_1:41
.= (B \ {u}) \ {(0. V)} by XBOOLE_1:41 ;
then C5: Lin ((B \ {(0. V)}) \ {u}) is free by C1, C4;
(Lin ((B \ {(0. V)}) \ {u})) + (Lin {u}) = Lin (((B \ {(0. V)}) \ {u}) \/ {u}) by ZMODUL02:72
.= Lin ((B \ {(0. V)}) \/ {u}) by XBOOLE_1:39
.= Lin (B \ {(0. V)}) by C3, ZFMISC_1:40 ;
hence Lin (B \ {(0. V)}) is free by C5; :: thesis: verum

end;

B4: for n being Nat holds S₁[n] from NAT_1:sch 2(B2, B3);
set n = card (A \ {(0. V)});
S₁[ card (A \ {(0. V)})] by B4;
hence Lin (A \ {(0. V)}) is free ; :: thesis: verum

end;

per cases ( 0. V in A or not 0. V in A ) ;

suppose B1: 0. V in A ; :: thesis: V is free

B2: Lin {(0. V)} = (0). V by ThLin5;
V is_the_direct_sum_of Lin (A \ {(0. V)}), Lin {(0. V)}

proof

(Lin (A \ {(0. V)})) + (Lin {(0. V)}) = Lin ((A \ {(0. V)}) \/ {(0. V)}) by ZMODUL02:72
.= Lin (A \/ {(0. V)}) by XBOOLE_1:39
.= Lin A by B1, ZFMISC_1:40 ;
hence V is_the_direct_sum_of Lin (A \ {(0. V)}), Lin {(0. V)} by A2, B2, ZMODUL01:107; :: thesis: verum

end;

hence V is free by A3, ZMODUL04:30; :: thesis: verum

end;

suppose not 0. V in A ; :: thesis: V is free

then Lin A is free by A3, ZFMISC_1:57;
hence V is free by A2, ZMODUL04:21; :: thesis: verum

end;

end;