defpred S₁[ 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 F_Rat ) holds
Sum F in F_Rat ;
P1: S₁[ 0 ]

proof

let F be FinSequence of F_Real; :: thesis:
assume AS1: ( len F = 0 & ( for i being Nat st i in dom F holds
F . i in F_Rat ) ) ; :: thesis:
F = <*> the carrier of F_Real by AS1;
then Sum F = 0. F_Real by RLVECT_1:43
.= 0 ;
hence Sum F in F_Rat ; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
assume AS1: S₁[n] ; :: thesis:
let F be FinSequence of F_Real; :: thesis:
assume AS2: ( len F = n + 1 & ( for i being Nat st i in dom F holds
F . i in F_Rat ) ) ; :: thesis:
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;
len F = (len F0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;
then P3: Sum F = (Sum F0) + af by AS2, P4, RLVECT_1:38;
for i being Nat st i in dom F0 holds
F0 . i in F_Rat

proof

let i be Nat; :: thesis:
assume P40: i in dom F0 ; :: thesis:
dom F = Seg (n + 1) by AS2, FINSEQ_1:def 3;
then dom F0 c= dom F by P4, FINSEQ_1:5, NAT_1:11;
then F . i in F_Rat by AS2, P40;
hence F0 . i in F_Rat by P40, FUNCT_1:47; :: thesis:

end;

then Sum F0 in F_Rat by P1, AS1;
then reconsider i1 = Sum F0 as Element of F_Rat ;
F . (n + 1) in F_Rat by A70, AS2;
then reconsider i2 = af as Element of F_Rat ;
Sum F = i1 + i2 by P3;
hence Sum F in F_Rat ; :: thesis:

end;

X1: for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
let F be FinSequence of F_Real; :: thesis:
assume X2: for i being Nat st i in dom F holds
F . i in F_Rat ; :: thesis:
len F is Nat ;
hence Sum F in F_Rat by X1, X2; :: thesis: