defpred S_{1}[ Nat] means for F being FinSequence of F_Real

for G being FinSequence of F_Rat st len F = $1 & F = G holds

Sum F = Sum G;

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 G being FinSequence of F_Rat st F = G holds

Sum F = Sum G

let G be FinSequence of F_Rat; :: thesis: ( F = G implies Sum F = Sum G )

assume F = G ; :: thesis: Sum F = Sum G

hence Sum F = Sum G by X1; :: thesis: verum

for G being FinSequence of F_Rat st len F = $1 & F = G holds

Sum F = Sum G;

P1: S

proof

P2:
for n being Nat st S
let F be FinSequence of F_Real; :: thesis: for G being FinSequence of F_Rat st len F = 0 & F = G holds

Sum F = Sum G

let G be FinSequence of F_Rat; :: thesis: ( len F = 0 & F = G implies Sum F = Sum G )

assume AS1: ( len F = 0 & F = G ) ; :: thesis: Sum F = Sum G

F = <*> the carrier of F_Real by AS1;

then X1: Sum F = 0. F_Real by RLVECT_1:43

.= 0 ;

G = <*> the carrier of F_Rat by AS1;

then Sum G = 0. F_Rat by RLVECT_1:43

.= 0 ;

hence Sum F = Sum G by X1; :: thesis: verum

end;Sum F = Sum G

let G be FinSequence of F_Rat; :: thesis: ( len F = 0 & F = G implies Sum F = Sum G )

assume AS1: ( len F = 0 & F = G ) ; :: thesis: Sum F = Sum G

F = <*> the carrier of F_Real by AS1;

then X1: Sum F = 0. F_Real by RLVECT_1:43

.= 0 ;

G = <*> the carrier of F_Rat by AS1;

then Sum G = 0. F_Rat by RLVECT_1:43

.= 0 ;

hence Sum F = Sum G by X1; :: 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: for G being FinSequence of F_Rat st len F = n + 1 & F = G holds

Sum F = Sum G

let G be FinSequence of F_Rat; :: thesis: ( len F = n + 1 & F = G implies Sum F = Sum G )

assume AS2: ( len F = n + 1 & F = G ) ; :: thesis: Sum F = Sum G

reconsider F0 = F | n as FinSequence of F_Real ;

reconsider G0 = G | n as FinSequence of F_Rat ;

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 ;

G . (n + 1) in rng G by AS2, A70, FUNCT_1:3;

then reconsider ag = G . (n + 1) as Element of F_Rat ;

P1: len F0 = n by FINSEQ_1:59, AS2, NAT_1:11;

len G0 = n by FINSEQ_1:59, AS2, NAT_1:11;

then BP4: dom G0 = Seg n by FINSEQ_1:def 3;

A9: len F = (len F0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;

BP3: Sum G = (Sum G0) + ag by AS2, A9, BP4, RLVECT_1:38;

(Sum F0) + af = (Sum G0) + ag by AS1, AS2, P1;

hence Sum F = Sum G by AS2, A9, BP3, BP4, RLVECT_1:38; :: thesis: verum

end;assume AS1: S

let F be FinSequence of F_Real; :: thesis: for G being FinSequence of F_Rat st len F = n + 1 & F = G holds

Sum F = Sum G

let G be FinSequence of F_Rat; :: thesis: ( len F = n + 1 & F = G implies Sum F = Sum G )

assume AS2: ( len F = n + 1 & F = G ) ; :: thesis: Sum F = Sum G

reconsider F0 = F | n as FinSequence of F_Real ;

reconsider G0 = G | n as FinSequence of F_Rat ;

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 ;

G . (n + 1) in rng G by AS2, A70, FUNCT_1:3;

then reconsider ag = G . (n + 1) as Element of F_Rat ;

P1: len F0 = n by FINSEQ_1:59, AS2, NAT_1:11;

len G0 = n by FINSEQ_1:59, AS2, NAT_1:11;

then BP4: dom G0 = Seg n by FINSEQ_1:def 3;

A9: len F = (len F0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;

BP3: Sum G = (Sum G0) + ag by AS2, A9, BP4, RLVECT_1:38;

(Sum F0) + af = (Sum G0) + ag by AS1, AS2, P1;

hence Sum F = Sum G by AS2, A9, BP3, BP4, RLVECT_1:38; :: thesis: verum

let F be FinSequence of F_Real; :: thesis: for G being FinSequence of F_Rat st F = G holds

Sum F = Sum G

let G be FinSequence of F_Rat; :: thesis: ( F = G implies Sum F = Sum G )

assume F = G ; :: thesis: Sum F = Sum G

hence Sum F = Sum G by X1; :: thesis: verum