theorem Th1: :: BASEL_2:1

for n being Nat
for z being Complex
for e being Element of F_Complex st z = e holds
n * z = n * e