let n be non zero Nat; :: thesis: for h, g being FinSequence of REAL n 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 REAL n; :: 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
per cases ( len g = 0 or len g > 0 ) ;
suppose A3: len g = 0 ; :: thesis: (h /. 1) - (h /. (len h)) = Sum g
then (h /. 1) - (h /. (len h)) = 0* n by A1, EUCLIDLP:9;
hence (h /. 1) - (h /. (len h)) = Sum g by A3, EUCLID_7:def 11; :: thesis: verum
end;
suppose A4: len g > 0 ; :: thesis: (h /. 1) - (h /. (len h)) = Sum g
then A5: Sum g = (accum g) . (len g) by EUCLID_7:def 11;
defpred S1[ Nat] means ( $1 <= len g implies (accum g) . $1 = (h /. 1) - (h /. ($1 + 1)) );
A6: S1[1]
proof
assume 1 <= len g ; :: thesis: (accum g) . 1 = (h /. 1) - (h /. (1 + 1))
then 1 in Seg (len g) ;
then A7: 1 in dom g by FINSEQ_1:def 3;
(accum g) . 1 = g . 1 by EUCLID_7:def 10;
then (accum g) . 1 = g /. 1 by A7, PARTFUN1:def 6;
hence (accum g) . 1 = (h /. 1) - (h /. (1 + 1)) by A7, A2; :: thesis: verum
end;
A8: for j being Nat st 1 <= j & S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( 1 <= j & S1[j] implies S1[j + 1] )
assume A9: 1 <= j ; :: thesis: ( not S1[j] or S1[j + 1] )
assume A10: S1[j] ; :: thesis: S1[j + 1]
assume A11: j + 1 <= len g ; :: thesis: (accum g) . (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;
len g = len (accum g) by EUCLID_7:def 10;
then A14: j in dom (accum g) by A9, A12, FINSEQ_3:25;
(accum g) . (j + 1) = ((accum g) /. j) + (g /. (j + 1)) by A9, A12, EUCLID_7:def 10;
then A15: (accum g) . (j + 1) = ((accum g) /. j) + ((h /. (j + 1)) - (h /. ((j + 1) + 1))) by A2, A13;
reconsider hj1 = h /. (j + 1) as Point of (TOP-REAL n) by EUCLID:22;
reconsider hj2 = h /. (j + 2) as Point of (TOP-REAL n) by EUCLID:22;
reconsider hj3 = (h /. 1) - (h /. (j + 1)) as Point of (TOP-REAL n) by EUCLID:22;
(accum g) . (j + 1) = hj3 + (hj1 - hj2) by A15, A10, A11, A14, NAT_1:13, PARTFUN1:def 6;
then (accum g) . (j + 1) = (hj3 + hj1) - hj2 by RLVECT_1:def 3;
hence (accum g) . (j + 1) = (h /. 1) - (h /. ((j + 1) + 1)) by RVSUM_1:43; :: thesis: verum
end;
A16: 1 <= len g by A4, NAT_1:14;
for i being Nat st 1 <= i holds
S1[i] from NAT_1:sch 8(A6, A8);
hence (h /. 1) - (h /. (len h)) = Sum g by A5, A1, A16; :: thesis: verum
end;
end;