theorem Th11: :: FLEXARY1:11

for k being Nat
for f being complex-valued Function holds (f,k) +...+ (f,k) = f . k