theorem Th21: :: HILB10_4:21

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