defpred S1[ Nat] means for F being FinSequence of F_Real st len F = $1 & ( for i being Nat st i in dom F holds
F . i in INT ) holds
Sum F in INT ;
P1:
S1[ 0 ]
P2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume AS1:
S1[
n]
;
S1[n + 1]
let F be
FinSequence of
F_Real;
( len F = n + 1 & ( for i being Nat st i in dom F holds
F . i in INT ) implies Sum F in INT )
assume AS2:
(
len F = n + 1 & ( for
i being
Nat st
i in dom F holds
F . i in INT ) )
;
Sum F in INT
reconsider F0 =
F | n as
FinSequence of
F_Real ;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then A70:
n + 1
in dom F
by AS2, FINSEQ_1:def 3;
then
F . (n + 1) in rng F
by FUNCT_1:3;
then reconsider af =
F . (n + 1) as
Element of
F_Real ;
P1:
len F0 = n
by FINSEQ_1:59, AS2, NAT_1:11;
then P4:
dom F0 = Seg n
by FINSEQ_1:def 3;
A9:
len F = (len F0) + 1
by AS2, FINSEQ_1:59, NAT_1:11;
A11:
F0 = F | (dom F0)
by P4, FINSEQ_1:def 15;
then P3:
Sum F = (Sum F0) + af
by AS2, A9, RLVECT_1:38;
for
i being
Nat st
i in dom F0 holds
F0 . i in INT
then
Sum F0 in INT
by P1, AS1;
then reconsider i1 =
Sum F0 as
Integer ;
F . (n + 1) in INT
by A70, AS2;
then reconsider i2 =
af as
Integer ;
Sum F = i1 + i2
by P3;
hence
Sum F in INT
by INT_1:def 2;
verum
end;
X1:
for n being Nat holds S1[n]
from NAT_1:sch 2(P1, P2);
let F be FinSequence of F_Real; ( ( for i being Nat st i in dom F holds
F . i in INT ) implies Sum F in INT )
assume X2:
for i being Nat st i in dom F holds
F . i in INT
; Sum F in INT
len F is Nat
;
hence
Sum F in INT
by X1, X2; verum