defpred S_{1}[ 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_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[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

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

proof

P2:
for n being Nat st S
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;( 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

S

proof

P3:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume AS1: S_{1}[n]
; :: thesis: S_{1}[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

( a <> 0 & ( for r being Element of RAT st r in X holds

a * r in INT ) ) by A4, A6; :: thesis: verum

end;assume AS1: S

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

hence
ex a being Element of INT st
let r be Element of RAT ; :: thesis: ( r in X implies a * r in INT )

assume r in X ; :: thesis: a * r in INT

end;assume r in X ; :: thesis: a * r in INT

( a <> 0 & ( for r being Element of RAT st r in X holds

a * r in INT ) ) by A4, A6; :: thesis: verum

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