for n being Nat
for c being Element of COMPLEX
for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2) by Th54, FINSEQOP:51, FINSEQOP:54;