let x, y be Real; :: thesis: ( |.x.| <= |.(x + (y * <i>)).| & |.y.| <= |.(x + (y * <i>)).| )
set z = x + (y * <i>);
( Re (x + (y * <i>)) = x & Im (x + (y * <i>)) = y ) by COMPLEX1:12;
hence ( |.x.| <= |.(x + (y * <i>)).| & |.y.| <= |.(x + (y * <i>)).| ) by COMPLEX1:79; :: thesis: verum