set ZS = Rat-Module ;
defpred S₁[ Nat] means for A being finite Subset of Rat-Module st card A = $1 holds
ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) );
P0: S₁[ 0 ]

proof

let A be finite Subset of Rat-Module; :: thesis: ( card A = 0 implies ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) ) )
assume card A = 0 ; :: thesis: ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )
then P2: A = {} the carrier of Rat-Module ;
P3: the carrier of ((0). Rat-Module) = {(0. Rat-Module)} by VECTSP_4:def 3;
reconsider n = 1 as Integer ;
take n ; :: thesis: ( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )
thus n <> 0 ; :: thesis: for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n
let s be Element of Rat-Module; :: thesis: ( s in Lin A implies ex m being Integer st s = m / n )
assume s in Lin A ; :: thesis: ex m being Integer st s = m / n
then P4: s in (0). Rat-Module by P2, ZMODUL02:67;
reconsider m = 0 as Integer ;
take m ; :: thesis: s = m / n
thus s = m / n by P3, P4, TARSKI:def 1; :: thesis: verum

end;

P1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume P11: S₁[k] ; :: thesis: S₁[k + 1]
let A be finite Subset of Rat-Module; :: thesis: ( card A = k + 1 implies ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) ) )
assume B3: card A = k + 1 ; :: thesis: ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )
then A <> {} ;
then consider v being object such that
B4: v in A by XBOOLE_0:7;
reconsider v = v as VECTOR of Rat-Module by B4;
set Av = A \ {v};
B6: {v} is Subset of A by B4, SUBSET_1:41;
then card (A \ {v}) = (k + 1) - (card {v}) by B3, CARD_2:44
.= (k + 1) - 1 by CARD_1:30
.= k ;
then consider nk being Integer such that
B8: ( nk <> 0 & ( for s being Element of Rat-Module st s in Lin (A \ {v}) holds
ex mk being Integer st s = mk / nk ) ) by P11;
consider mv, nv being Integer such that
B9: ( nv > 0 & v = mv / nv ) by RAT_1:1;
reconsider n = nk * nv as Integer ;
take n ; :: thesis: ( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )
thus n <> 0 by B8, B9; :: thesis: for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n
A = (A \ {v}) \/ {v} by B6, XBOOLE_1:45;
then B11: Lin A = (Lin (A \ {v})) + (Lin {v}) by ZMODUL02:72;
let s be Element of Rat-Module; :: thesis: ( s in Lin A implies ex m being Integer st s = m / n )
assume s in Lin A ; :: thesis: ex m being Integer st s = m / n
then consider sk, sv being VECTOR of Rat-Module such that
B12: ( sk in Lin (A \ {v}) & sv in Lin {v} & s = sk + sv ) by ZMODUL01:92, B11;
consider mk being Integer such that
B13: sk = mk / nk by B8, B12;
consider l being Linear_Combination of {v} such that
B14: sv = Sum l by B12, ZMODUL02:64;
B15: Sum l = (l . v) * v by ZMODUL02:21;
reconsider k = l . v as Integer ;
B16: sv = k * (mv / nv) by B9, B14, B15, LMTFRat2;
reconsider m = (mk * nv) + ((k * mv) * nk) as Integer ;
take m ; :: thesis: s = m / n
reconsider s1 = mk / nk as Rational ;
reconsider ss1 = s1 as Element of F_Rat by RAT_1:def 1;
reconsider mn = mv / nv as Rational ;
reconsider s2 = k * mn as Rational ;
reconsider ss2 = s2 as Element of F_Rat by RAT_1:def 2;
reconsider sss1 = ss1, sss2 = ss2 as Element of F_Real by TARSKI:def 3, GAUSSINT:13;
XX1: ss1 + ss2 = sss1 + sss2
.= (mk / nk) + (k * (mv / nv)) ;
thus s = ((mk * nv) / (nk * nv)) + ((k * mv) / nv) by B9, B12, B13, B16, XX1, XCMPLX_1:91
.= ((mk * nv) / (nk * nv)) + (((k * mv) * nk) / (nv * nk)) by B8, XCMPLX_1:91
.= m / n ; :: thesis: verum

end;

P2: for k being Nat holds S₁[k] from NAT_1:sch 2(P0, P1);
let A be finite Subset of Rat-Module; :: thesis: ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )
card A is Nat ;
hence ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) ) by P2; :: thesis: verum