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 F_Rat ) holds
Sum F in F_Rat ;
P1: S1[ 0 ]
proof
let F be FinSequence of F_Real; :: thesis: ( len F = 0 & ( for i being Nat st i in dom F holds
F . i in F_Rat ) implies Sum F in F_Rat )

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: 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 F be FinSequence of F_Real; :: thesis: ( len F = n + 1 & ( for i being Nat st i in dom F holds
F . i in F_Rat ) implies Sum F in F_Rat )

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 ;
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 ;
then P4: dom F0 = Seg n by FINSEQ_1:def 3;
len F = (len F0) + 1 by ;
then P3: Sum F = (Sum F0) + af by ;
for i being Nat st i in dom F0 holds
F0 . i in F_Rat
proof
let i be Nat; :: thesis: ( i in dom F0 implies F0 . i in F_Rat )
assume P40: i in dom F0 ; :: thesis: F0 . i in F_Rat
dom F = Seg (n + 1) by ;
then dom F0 c= dom F by ;
then F . i in F_Rat by ;
hence F0 . i in F_Rat by ; :: thesis: verum
end;
then Sum F0 in F_Rat by ;
then reconsider i1 = Sum F0 as Element of F_Rat ;
F . (n + 1) in F_Rat by ;
then reconsider i2 = af as Element of F_Rat ;
Sum F = i1 + i2 by P3;
hence Sum F in F_Rat ; :: thesis: verum
end;
X1: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
let F be FinSequence of F_Real; :: thesis: ( ( for i being Nat st i in dom F holds
F . i in F_Rat ) implies Sum F in F_Rat )

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