let F, G, H be FinSequence of REAL ; :: thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ) implies Sum H = (Sum F) - (Sum G) )
assume that
A1: ( len F = len G & len F = len H ) and
A2: for k being Element of NAT st k in dom F holds
H . k = (F /. k) - (G /. k) ; :: thesis: Sum H = (Sum F) - (Sum G)
A3: for k being Element of NAT st k in dom F holds
H . k = (F . k) - (G . k)

proof

let k be Element of NAT ; :: thesis: ( k in dom F implies H . k = (F . k) - (G . k) )
assume A4: k in dom F ; :: thesis: H . k = (F . k) - (G . k)
then A5: F /. k = F . k by PARTFUN1:def 8;
k in Seg (len G) by A1, A4, FINSEQ_1:def 3;
then k in dom G by FINSEQ_1:def 3;
then G /. k = G . k by PARTFUN1:def 8;
hence H . k = (F . k) - (G . k) by A2, A4, A5; :: thesis: verum

end;

A6: F is Element of (len F) -tuples_on REAL by FINSEQ_2:110;
A7: G is Element of (len F) -tuples_on REAL by A1, FINSEQ_2:110;
then A8: F - G is Element of (len F) -tuples_on REAL by A6, FINSEQ_2:140;
then A9: len H = len (F - G) by A1, FINSEQ_1:def 18;
then X: dom H = Seg (len (F - G)) by FINSEQ_1:def 3;
for k being Nat st k in dom H holds
H . k = (F - G) . k

proof

let k be Nat; :: thesis: ( k in dom H implies H . k = (F - G) . k )
assume A10: k in dom H ; :: thesis: H . k = (F - G) . k
then k in Seg (len F) by A8, X, FINSEQ_1:def 18;
then k in dom F by FINSEQ_1:def 3;
then A11: H . k = (F . k) - (G . k) by A3;
k in dom (F - G) by A10, X, FINSEQ_1:def 3;
hence H . k = (F - G) . k by A11, VALUED_1:13; :: thesis: verum

end;

then Sum H = Sum (F - G) by A9, FINSEQ_2:10
.= (Sum F) - (Sum G) by A6, A7, RVSUM_1:120 ;
hence Sum H = (Sum F) - (Sum G) ; :: thesis: verum