theorem :: RVSUM_2:14

for i being Nat
for c1, c2 being Complex holds (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)