let i be Nat; :: thesis: for R1, R2 being i -element complex-valued FinSequence holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be i -element complex-valued FinSequence; :: thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
thus Sum (R1 - R2) = (Sum R1) + (Sum (- R2)) by Th40
.= (Sum R1) - (Sum R2) by Th39 ; :: thesis: verum