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