defpred S1[ 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: S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AS1: S1[n] ; :: thesis: S1[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 ;
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 ;
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 ;
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 ;
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 S1[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