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

proof

let k be Element of NAT ; :: thesis: ( k in dom q1 implies q . k = (q1 /. k) - (q2 /. k) )
assume A4: k in dom q1 ; :: thesis: q . k = (q1 /. k) - (q2 /. k)
A5: k in dom q2 by A2, A4, FINSEQ_3:29;
thus q . k = (q1 . k) - (q2 . k) by A3, A4
.= (q1 /. k) - (q2 . k) by A4, PARTFUN1:def 6
.= (q1 /. k) - (q2 /. k) by A5, PARTFUN1:def 6 ; :: thesis: verum

end;

hence Sum q = (Sum q1) - (Sum q2) by A1, A2, INTEGRA1:22; :: thesis: verum