let z1, z2 be Complex; :: thesis: cpx2euc (z1 - z2) = (cpx2euc z1) - (cpx2euc z2)
thus cpx2euc (z1 - z2) = cpx2euc (z1 + (- z2))
.= (cpx2euc z1) + (cpx2euc (- z2)) by Th7
.= (cpx2euc z1) - (cpx2euc z2) by Th11 ; :: thesis: verum