let x1, x2 be Real; :: thesis: cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]|
Re (x1 + (x2 * <i>)) = x1 by COMPLEX1:12;
hence cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]| by COMPLEX1:12; :: thesis: verum