theorem Th57: :: AFINSQ_2:58

for n being Nat
for c being Complex holds Sum (n --> c) = n * c