let i be Nat; :: thesis: for R1, R2 being i -long FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be i -long FinSequence of COMPLEX ; :: thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
thus Sum (R1 - R2) = (Sum R1) + (Sum (- R2)) by Th119
.= (Sum R1) - (Sum R2) by Th118 ; :: thesis: verum