let z1, z2 be Complex; :: thesis: ( cpx2euc z1 = cpx2euc z2 implies z1 = z2 )
assume A1: cpx2euc z1 = cpx2euc z2 ; :: thesis: z1 = z2
z2 = euc2cpx (cpx2euc z2) by Th1;
hence z1 = z2 by A1, Th1; :: thesis: verum