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