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

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

ex K being Integer st

( K <> 0 & ( for i being Nat st i in Seg $1 holds

K * (r /. i) in INT ) );

P1: S

proof

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

S

proof

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 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

end;assume AS1: S

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;

end;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 )
;

end;

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;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

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