set ZS = Rat-Module ;
defpred S₁[ Nat] means for A being finite Subset of Rat-Module st card A = $1 holds
rank (Lin A) <= 1;
A1: S₁[ 0 ]

proof

let A be finite Subset of Rat-Module; :: thesis: ( card A = 0 implies rank (Lin A) <= 1 )
assume B1: card A = 0 ; :: thesis: rank (Lin A) <= 1
A = {} the carrier of Rat-Module by B1;
then Lin A = (0). Rat-Module by ZMODUL02:67
.= (0). (Lin A) by ZMODUL01:51 ;
then (Omega). (Lin A) = (0). (Lin A) ;
hence rank (Lin A) <= 1 by ZMODUL05:1; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
let A be finite Subset of Rat-Module; :: thesis: ( card A = n + 1 implies rank (Lin A) <= 1 )
assume B2: card A = n + 1 ; :: thesis: rank (Lin A) <= 1
A <> {} by B2;
then consider x being object such that
B3: x in A by XBOOLE_0:7;
reconsider x = x as VECTOR of Rat-Module by B3;
B5: card (A \ {x}) = (card A) - (card {x}) by B3, ZFMISC_1:31, CARD_2:44
.= (n + 1) - 1 by B2, CARD_1:30
.= n ;
B6: (Lin (A \ {x})) + (Lin {x}) = Lin ((A \ {x}) \/ {x}) by ZMODUL02:72
.= Lin (A \/ {x}) by XBOOLE_1:39
.= Lin A by B3, ZFMISC_1:40 ;

per cases ( rank (Lin (A \ {x})) = 0 or rank (Lin (A \ {x})) = 1 ) by B1, B5, NAT_1:25;

suppose rank (Lin (A \ {x})) = 0 ; :: thesis: rank (Lin A) <= 1

then C2: (Omega). (Lin (A \ {x})) = (0). (Lin (A \ {x})) by ZMODUL05:1
.= (0). Rat-Module by ZMODUL01:51 ;

per cases ( x = 0. Rat-Module or x <> 0. Rat-Module ) ;

suppose x = 0. Rat-Module ; :: thesis: rank (Lin A) <= 1

then Lin {x} = (0). Rat-Module by ZMODUL06:22;
then (Lin (A \ {x})) + (Lin {x}) = (0). Rat-Module by C2, ZMODUL01:99;
then (Omega). (Lin A) = (0). (Lin A) by B6, ZMODUL01:51;
hence rank (Lin A) <= 1 by ZMODUL05:1; :: thesis: verum

end;

suppose D1: x <> 0. Rat-Module ; :: thesis: rank (Lin A) <= 1

reconsider Linx = Lin {x} as free Submodule of Rat-Module ;
x in Lin A by B3, ZMODUL02:65;
then reconsider xx = x as VECTOR of (Lin A) ;
Lin A = Lin {x} by B6, C2, ZMODUL01:99
.= Lin {xx} by ZMODUL03:20 ;
then D3: (Omega). (Lin A) = Lin {xx} ;
xx <> 0. (Lin A) by D1, ZMODUL01:26;
hence rank (Lin A) <= 1 by D3, ZMODUL05:5; :: thesis: verum

end;

end;

end;

suppose rank (Lin (A \ {x})) = 1 ; :: thesis: rank (Lin A) <= 1

then consider axl being VECTOR of (Lin (A \ {x})) such that
C2: ( axl <> 0. (Lin (A \ {x})) & (Omega). (Lin (A \ {x})) = Lin {axl} ) by ZMODUL05:5;
reconsider ax = axl as VECTOR of Rat-Module by ZMODUL01:25;
C3: ax <> 0. Rat-Module by C2, ZMODUL01:26;
C4: Lin (A \ {x}) = Lin {ax} by C2, ZMODUL03:20;
C5: {ax} is linearly-independent by C3, ZMODUL02:59;

per cases ( x = 0. Rat-Module or x = ax or ( x <> 0. Rat-Module & x <> ax ) ) ;

suppose x = 0. Rat-Module ; :: thesis: rank (Lin A) <= 1

then Lin {x} = (0). Rat-Module by ZMODUL06:22;
then (Lin (A \ {x})) + (Lin {x}) = Lin (A \ {x}) by ZMODUL01:99;
hence rank (Lin A) <= 1 by B1, B5, B6; :: thesis: verum

end;

suppose x = ax ; :: thesis: rank (Lin A) <= 1

then (Lin (A \ {x})) + (Lin {x}) = Lin (A \ {x}) by C4, ZMODUL01:95;
hence rank (Lin A) <= 1 by B1, B5, B6; :: thesis: verum

end;

suppose D1: ( x <> 0. Rat-Module & x <> ax ) ; :: thesis: rank (Lin A) <= 1

then D2: {x} is linearly-independent by ZMODUL02:59;
{ax,x} is linearly-dependent by D1, LMThFRat32;
then D3: {ax} \/ {x} is linearly-dependent by ENUMSET1:1;
{ax} /\ {x} = {} by D1, XBOOLE_0:def 7, ZFMISC_1:11;
then D4: (Lin {ax}) /\ (Lin {x}) <> (0). Rat-Module by C5, D2, D3, ZMODUL06:23;
consider y being VECTOR of Rat-Module such that
D5: ( y <> 0. Rat-Module & (Lin {ax}) + (Lin {x}) = Lin {y} ) by C3, D1, D4, ZMODUL06:28;
D6: y <> 0. (Lin A) by D5, ZMODUL01:26;
y in Lin A by B6, C4, D5, ZMODUL06:20;
then reconsider yy = y as VECTOR of (Lin A) ;
(Omega). (Lin A) = Lin {yy} by B6, C4, D5, ZMODUL03:20;
hence rank (Lin A) <= 1 by D6, ZMODUL05:5; :: thesis: verum

end;

end;

end;

end;

end;

A3: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let A be finite Subset of Rat-Module; :: thesis: rank (Lin A) <= 1
set n = card A;
S₁[ card A] by A3;
hence rank (Lin A) <= 1 ; :: thesis: verum