theorem Th7: :: EUCLID_3:7

for z1, z2 being Complex holds cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2)