let x, y be Complex; :: thesis: 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2)
set a = |.x.|;
set b = |.y.|;
(|.x.| - |.y.|) ^2 = ((|.x.| * |.x.|) - ((|.x.| * |.y.|) + (|.x.| * |.y.|))) + (|.y.| * |.y.|) ;
then ( |.x.| * |.y.| = |.(x * y).| & ((|.x.| * |.x.|) + (|.y.| * |.y.|)) - ((|.x.| * |.y.|) + (|.x.| * |.y.|)) >= 0 ) by COMPLEX1:65, XREAL_1:63;
hence 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by XREAL_1:49; :: thesis: verum