theorem :: RVSUM_2:6

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