let Y be RealNormSpace; :: thesis: for xseq, yseq being FinSequence of Y st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Point of Y st
( v = xseq /. (len xseq) & Sum xseq = (Sum yseq) + v )
let xseq, yseq be FinSequence of Y; :: thesis: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq implies ex v being Point of Y 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 Point of Y 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 A2: v = xseq . (len xseq) by PARTFUN1:def 6;
xseq | (len yseq) = xseq | (dom yseq) by FINSEQ_1:def 3;
hence ( v = xseq /. (len xseq) & Sum xseq = (Sum yseq) + v ) by A1, A2, RLVECT_1:38; :: thesis: verum