defpred S₁[ Nat] means for X being finite Subset of RAT st card X = $1 holds
ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) );
P1: S₁[ 0 ]

proof

let X be finite Subset of RAT; :: thesis: ( card X = 0 implies ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) )
assume AS: card X = 0 ; :: thesis: ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
reconsider a = 1 as Element of INT by NUMBERS:17;
take a ; :: thesis: ( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
thus a <> 0 ; :: thesis: for r being Element of RAT st r in X holds
a * r in INT
thus for r being Element of RAT st r in X holds
a * r in INT by AS; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume AS1: S₁[n] ; :: thesis: S₁[n + 1]
let X be finite Subset of RAT; :: thesis: ( card X = n + 1 implies ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) )
assume AS2: card X = n + 1 ; :: thesis: ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
then X <> {} ;
then consider x being object such that
A1: x in X by XBOOLE_0:def 1;
B6: {x} is Subset of X by A1, SUBSET_1:41;
set Y = X \ {x};
reconsider Y = X \ {x} as finite Subset of RAT ;
D1: X = Y \/ {x} by B6, XBOOLE_1:45;
card Y = (card X) - (card {x}) by B6, CARD_2:44
.= (n + 1) - 1 by AS2, CARD_1:30
.= n ;
then consider a0 being Element of INT such that
A4: a0 <> 0 and
A5: for r being Element of RAT st r in Y holds
a0 * r in INT by AS1;
reconsider x = x as Element of RAT by A1;
consider x0, ib0 being Integer such that
A6: ( ib0 > 0 & x = x0 / ib0 ) by RAT_1:1;
reconsider ia0 = a0 as Integer ;
set ia = ia0 * ib0;
reconsider a = ia0 * ib0 as Element of INT by INT_1:def 2;
for r being Element of RAT st r in X holds
a * r in INT

proof

let r be Element of RAT ; :: thesis: ( r in X implies a * r in INT )
assume r in X ; :: thesis: a * r in INT

per cases then ( r in Y or r in {x} ) by D1, XBOOLE_0:def 3;

suppose r in Y ; :: thesis: a * r in INT

then reconsider iar = ia0 * r as Integer by A5, INT_1:def 2;
a * r = ib0 * iar ;
hence a * r in INT by INT_1:def 2; :: thesis: verum

end;

suppose A72: r in {x} ; :: thesis: a * r in INT

a * r = ia0 * (ib0 * r)
.= ia0 * (ib0 * (x0 / ib0)) by A6, A72, TARSKI:def 1
.= ia0 * x0 by A6, XCMPLX_1:87 ;
hence a * r in INT by INT_1:def 2; :: thesis: verum

end;

end;

end;

hence ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) by A4, A6; :: thesis: verum

end;

P3: for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
let X be finite Subset of RAT; :: thesis: ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
card X is Nat ;
hence ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) ) by P3; :: thesis: verum