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 ]

let r be FinSequence of F_Rat; :: thesis:
assume len r = 0 ; :: thesis:
set K = 1;
take 1 ; :: thesis:
thus 1 <> 0 ; :: thesis:
thus for i being Nat st i in Seg 0 holds
1 * (r /. i) in INT ; :: thesis:

end;

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

let n be Nat; :: thesis:
assume AS1: S₁[n] ; :: thesis:
let r be FinSequence of F_Rat; :: thesis:
assume AS2: len r = n + 1 ; :: thesis:
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:
thus L0 * K0 <> 0 by Q0, Q1; :: thesis:
thus for i being Nat st i in Seg (n + 1) holds
(L0 * K0) * (r /. i) in INT :: thesis:

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:

end;

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:

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: