defpred S₁[ Nat] means for r being FinSequence of F_Rat st len r = $1 holds
ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg $1 holds
K * (r /. i) in INT ) );
P1: S₁[ 0 ]

proof

let r be FinSequence of F_Rat; :: thesis: ( len r = 0 implies ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg 0 holds
K * (r /. i) in INT ) ) )
assume len r = 0 ; :: thesis: ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg 0 holds
K * (r /. i) in INT ) )
set K = 1;
take 1 ; :: thesis: ( 1 <> 0 & ( for i being Nat st i in Seg 0 holds
1 * (r /. i) in INT ) )
thus 1 <> 0 ; :: thesis: for i being Nat st i in Seg 0 holds
1 * (r /. i) in INT
thus for i being Nat st i in Seg 0 holds
1 * (r /. i) in INT ; :: 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 r be FinSequence of F_Rat; :: thesis: ( len r = n + 1 implies ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg (n + 1) holds
K * (r /. i) in INT ) ) )
assume AS2: len r = n + 1 ; :: thesis: ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg (n + 1) holds
K * (r /. i) in INT ) )
reconsider r0 = r | n as FinSequence of F_Rat ;
consider L0 being Integer such that
Q0: ( L0 > 0 & L0 * (r /. (n + 1)) in INT ) by LMThGM2311;
P1: len r0 = n by FINSEQ_1:59, AS2, NAT_1:11;
then consider K0 being Integer such that
Q1: ( K0 <> 0 & ( for i being Nat st i in Seg n holds
K0 * (r0 /. i) in INT ) ) by AS1;
P4: dom r0 = Seg n by P1, FINSEQ_1:def 3;
set K = L0 * K0;
take L0 * K0 ; :: thesis: ( L0 * K0 <> 0 & ( for i being Nat st i in Seg (n + 1) holds
(L0 * K0) * (r /. i) in INT ) )
thus L0 * K0 <> 0 by Q0, Q1; :: thesis: for i being Nat st i in Seg (n + 1) holds
(L0 * K0) * (r /. i) in INT
thus for i being Nat st i in Seg (n + 1) holds
(L0 * K0) * (r /. i) in INT :: thesis: verum

proof

let i be Nat; :: thesis: ( i in Seg (n + 1) implies (L0 * K0) * (r /. i) in INT )
assume i in Seg (n + 1) ; :: thesis: (L0 * K0) * (r /. i) in INT
then Q3: ( 1 <= i & i <= n + 1 ) by FINSEQ_1:1;

per cases ( i <= n or i > n ) ;

suppose i <= n ; :: thesis: (L0 * K0) * (r /. i) in INT

then Q5: i in Seg n by Q3;
then K0 * (r0 /. i) in INT by Q1;
then reconsider KR = K0 * (r /. i) as Integer by P4, Q5, PARTFUN1:80;
reconsider iL0 = L0 as Integer ;
L0 * KR in INT by INT_1:def 2;
hence (L0 * K0) * (r /. i) in INT ; :: thesis: verum

end;

suppose i > n ; :: thesis: (L0 * K0) * (r /. i) in INT

then n + 1 <= i by NAT_1:13;
then reconsider LR = L0 * (r /. i) as Integer by Q0, Q3, XXREAL_0:1;
reconsider iK0 = K0 as Integer ;
K0 * LR in INT by INT_1:def 2;
hence (L0 * K0) * (r /. i) in INT ; :: thesis: verum

end;

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
hence for n being Nat
for r being FinSequence of F_Rat st len r = n holds
ex K being Integer st
( K <> 0 & ( for i being Nat st i in Seg n holds
K * (r /. i) in INT ) ) ; :: thesis: verum