let n be non zero Nat; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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)
proof
let i be Nat; :: thesis: ( i in dom h implies h /. i = (j /. i) + (g /. i) )
reconsider ji = j /. i, hi = h /. i, gi = g /. i as Point of (TOP-REAL n) by EUCLID:22;
assume i in dom h ; :: thesis: h /. i = (j /. i) + (g /. i)
then ji = hi - gi by A1, A2, A3;
then ji + gi = hi by RLVECT_4:1;
hence h /. i = (j /. i) + (g /. i) ; :: thesis: verum
end;
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 ; :: thesis: ( k in dom h implies h . k = (j + g) . k )
assume A6: k in dom h ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum