let xseq, yseq be FinSequence of REAL ; :: thesis: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq implies ex v being Real st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) )
assume A1: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq ) ; :: thesis: ex v being Real st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
take v = xseq . (len xseq); :: thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
len xseq in Seg (len xseq) by A1, FINSEQ_1:4;
then len xseq in dom xseq by FINSEQ_1:def 3;
then v = xseq /. (len xseq) by PARTFUN1:def 6;
then xseq = (xseq | (len yseq)) ^ <*v*> by A1, FINSEQ_5:21;
hence ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) by A1, RVSUM_1:74; :: thesis: verum