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