let F, G be FinSequence of INT ; :: thesis: for v being Integer st len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) holds

Sum F = (Sum G) + v

let v be Integer; :: thesis: ( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v )

assume that

A1: len F = (len G) + 1 and

A2: G = F | (dom G) and

A3: v = F . (len F) ; :: thesis: Sum F = (Sum G) + v

reconsider Fr = F, Gr = G as real-valued FinSequence ;

reconsider vr = v as Real ;

set k = len G;

dom G = Seg (len G) by FINSEQ_1:def 3;

then Fr = Gr ^ <*vr*> by A1, A2, A3, FINSEQ_3:55;

hence Sum F = (Sum G) + v by RVSUM_1:74; :: thesis: verum

Sum F = (Sum G) + v

let v be Integer; :: thesis: ( len F = (len G) + 1 & G = F | (dom G) & v = F . (len F) implies Sum F = (Sum G) + v )

assume that

A1: len F = (len G) + 1 and

A2: G = F | (dom G) and

A3: v = F . (len F) ; :: thesis: Sum F = (Sum G) + v

reconsider Fr = F, Gr = G as real-valued FinSequence ;

reconsider vr = v as Real ;

set k = len G;

dom G = Seg (len G) by FINSEQ_1:def 3;

then Fr = Gr ^ <*vr*> by A1, A2, A3, FINSEQ_3:55;

hence Sum F = (Sum G) + v by RVSUM_1:74; :: thesis: verum