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