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 Function of NAT, the carrier of S such that
ADF1: ( Sum g = F . (len g) & F . 0 = 0. S & ( for j being Element of 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 ADF1, 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)) );
A6: S₁[1]

proof

assume A60: 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 ADF1, A60
.= g /. 1 by ADF1, 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 A10: S₁[j] ; :: thesis: S₁[j + 1]
assume A11: j + 1 <= len g ; :: thesis: F . (j + 1) = (h /. 1) - (h /. ((j + 1) + 1))
then A12: j < len g by NAT_1:13;
1 <= j + 1 by XREAL_1:38;
then A13: j + 1 in dom g by A11, FINSEQ_3:25;
then A14: g . (j + 1) = g /. (j + 1) by PARTFUN1:def 6;
j is Element of NAT by ORDINAL1:def 12;
then F . (j + 1) = (F . j) + (g /. (j + 1)) by A14, A12, ADF1
.= (F . j) + ((h /. (j + 1)) - (h /. ((j + 1) + 1))) by A2, A13
.= (((h /. 1) - (h /. (j + 1))) + (h /. (j + 1))) - (h /. ((j + 1) + 1)) by A10, A11, 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;

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

end;

end;