theorem Th81: :: SEQ_4:82

for k, n being Nat
for c, c9 being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds
(c * z) . k = c * c9