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

S_{1}[n + 1]
_{1}[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: Sum F in F_Rat

len F is Nat ;

hence Sum F in F_Rat by X1, X2; :: thesis: verum

F . i in F_Rat ) holds

Sum F in F_Rat ;

P1: S

proof

P2:
for n being Nat st S
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: Sum F in F_Rat

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;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: Sum F in F_Rat

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

S

proof

X1:
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 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: Sum F in F_Rat

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

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

end;assume AS1: S

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: Sum F in F_Rat

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

then
Sum F0 in F_Rat
by P1, AS1;
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 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: verum

end;assume P40: i in dom F0 ; :: thesis: F0 . i in F_Rat

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

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

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: Sum F in F_Rat

len F is Nat ;

hence Sum F in F_Rat by X1, X2; :: thesis: verum