theorem :: EUCLID_3:14

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