let n be non zero Nat; for h, g, j being FinSequence of REAL n st len h = len j & len g = len j & ( for i being Nat st i in dom j holds
j /. i = (h /. i) - (g /. i) ) holds
Sum j = (Sum h) - (Sum g)
let h, g, j be FinSequence of REAL n; ( len h = len j & len g = len j & ( for i being Nat st i in dom j holds
j /. i = (h /. i) - (g /. i) ) implies Sum j = (Sum h) - (Sum g) )
assume that
A1:
( len h = len j & len g = len j )
and
A2:
for i being Nat st i in dom j holds
j /. i = (h /. i) - (g /. i)
; Sum j = (Sum h) - (Sum g)
A3:
( dom j = Seg (len j) & dom g = Seg (len g) & dom h = Seg (len h) )
by FINSEQ_1:def 3;
A4:
for i being Nat st i in dom h holds
h /. i = (j /. i) + (g /. i)
j + g = j <++> g
by INTEGR15:def 9;
then A5:
dom (j + g) = (dom j) /\ (dom g)
by VALUED_2:def 45;
reconsider Sj = Sum j, Sh = Sum h, Sg = Sum g as Point of (TOP-REAL n) by EUCLID:22;
for k being Element of NAT st k in dom h holds
h . k = (j + g) . k
proof
let k be
Element of
NAT ;
( k in dom h implies h . k = (j + g) . k )
assume A6:
k in dom h
;
h . k = (j + g) . k
then
h /. k = (j /. k) + (g /. k)
by A4;
then A7:
h . k = (j /. k) + (g /. k)
by A6, PARTFUN1:def 6;
(j + g) /. k = (j /. k) + (g /. k)
by A6, A1, A3, A5, INTEGR15:21;
hence
h . k = (j + g) . k
by A7, A6, A1, A3, A5, PARTFUN1:def 6;
verum
end;
then
Sh = Sj + Sg
by A1, A3, Th24, A5, PARTFUN1:5;
then
Sh - Sg = Sj
by RLVECT_4:1;
hence
(Sum h) - (Sum g) = Sum j
; verum