let S be RealNormSpace; :: thesis: for h, g being FinSequence of S st len h = (len g) + 1 & ( for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ) holds
(h /. 1) - (h /. (len h)) = Sum g
let h, g be FinSequence of S; :: thesis: ( len h = (len g) + 1 & ( for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ) implies (h /. 1) - (h /. (len h)) = Sum g )
assume that
A1: len h = (len g) + 1 and
A2: for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ; :: thesis: (h /. 1) - (h /. (len h)) = Sum g
consider F being sequence of the carrier of S such that
A3: ( Sum g = F . (len g) & F . 0 = 0. S & ( for j being Nat
for v being Element of S st j < len g & v = g . (j + 1) holds
F . (j + 1) = (F . j) + v ) ) by RLVECT_1:def 12;

per cases ( len g = 0 or len g > 0 ) ;

suppose len g = 0 ; :: thesis: (h /. 1) - (h /. (len h)) = Sum g

hence (h /. 1) - (h /. (len h)) = Sum g by A3, A1, RLVECT_1:15; :: thesis: verum

end;

suppose A4: len g > 0 ; :: thesis: (h /. 1) - (h /. (len h)) = Sum g

defpred S₁[ Nat] means ( $1 <= len g implies F . $1 = (h /. 1) - (h /. ($1 + 1)) );
A5: S₁[1]

proof

assume A6: 1 <= len g ; :: thesis: F . 1 = (h /. 1) - (h /. (1 + 1))
then 1 in Seg (len g) ;
then A7: 1 in dom g by FINSEQ_1:def 3;
reconsider zz0 = 0 as Element of NAT ;
g /. 1 = g . (zz0 + 1) by A7, PARTFUN1:def 6;
then F . (zz0 + 1) = (F . 0) + (g /. 1) by A3, A6
.= g /. 1 by A3, RLVECT_1:4 ;
hence F . 1 = (h /. 1) - (h /. (1 + 1)) by A7, A2; :: thesis: verum

end;

A8: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 1 <= j & S₁[j] implies S₁[j + 1] )
assume 1 <= j ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A9: S₁[j] ; :: thesis: S₁[j + 1]
assume A10: j + 1 <= len g ; :: thesis: F . (j + 1) = (h /. 1) - (h /. ((j + 1) + 1))
then A12: j + 1 in dom g by XREAL_1:38, FINSEQ_3:25;
then A13: g . (j + 1) = g /. (j + 1) by PARTFUN1:def 6;
F . (j + 1) = (F . j) + (g /. (j + 1)) by A13, A10, A3, NAT_1:13
.= (F . j) + ((h /. (j + 1)) - (h /. ((j + 1) + 1))) by A2, A12
.= (((h /. 1) - (h /. (j + 1))) + (h /. (j + 1))) - (h /. ((j + 1) + 1)) by A9, A10, NAT_1:13, RLVECT_1:28
.= ((h /. 1) - ((h /. (j + 1)) - (h /. (j + 1)))) - (h /. ((j + 1) + 1)) by RLVECT_1:29
.= ((h /. 1) - (0. S)) - (h /. ((j + 1) + 1)) by RLVECT_1:15 ;
hence F . (j + 1) = (h /. 1) - (h /. ((j + 1) + 1)) by RLVECT_1:13; :: thesis: verum

end;

A14: 1 <= len g by A4, NAT_1:14;
for i being Nat st 1 <= i holds
S₁[i] from NAT_1:sch 8(A5, A8);
hence (h /. 1) - (h /. (len h)) = Sum g by A3, A1, A14; :: thesis: verum

end;

end;