let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
let x, y be Point of X; :: thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
A1: ( y = H₁(X) implies |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) )

proof

assume A2: y = H₁(X) ; :: thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
then y .|. y = 0c by Def13;
hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A2, Th32, COMPLEX1:130, SQUARE_1:82; :: thesis: verum

end;

( y <> H₁(X) implies |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) )

proof

assume y <> H₁(X) ; :: thesis: |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)
then A3: y .|. y <> 0c by Def13;
reconsider c1 = |.(y .|. y).| + (0 * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
set c2 = - (x .|. y);
A4: ( Re (y .|. y) >= 0 & Im (y .|. y) = 0 ) by Def13;
then |.((Re (y .|. y)) + ((Im (y .|. y)) * <i> )).| = Re (y .|. y) by ABSVALUE:def 1;
then A5: |.(y .|. y).| = Re (y .|. y) by COMPLEX1:29;
then A6: y .|. y = c1 by A4, COMPLEX1:29;
((c1 * x) + ((- (x .|. y)) * y)) .|. ((c1 * x) + ((- (x .|. y)) * y)) = ((((c1 * (c1 *' )) * (x .|. x)) + ((c1 * ((- (x .|. y)) *' )) * (x .|. y))) + (((c1 *' ) * (- (x .|. y))) * (y .|. x))) + (((- (x .|. y)) * ((- (x .|. y)) *' )) * (y .|. y)) by Lm9
.= (((c1 * ((c1 *' ) * (x .|. x))) + (c1 * (((- (x .|. y)) *' ) * (x .|. y)))) + ((c1 *' ) * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *' ))) by A4, A5, COMPLEX1:29
.= ((c1 * (((c1 *' ) * (x .|. x)) + (((- (x .|. y)) *' ) * (x .|. y)))) + (c1 * ((- (x .|. y)) * (y .|. x)))) + (c1 * ((- (x .|. y)) * ((- (x .|. y)) *' ))) by A6, Def13
.= c1 * (((((c1 *' ) * (x .|. x)) + (((- (x .|. y)) *' ) * (x .|. y))) + ((- (x .|. y)) * (y .|. x))) + ((- (x .|. y)) * ((- (x .|. y)) *' )))
.= c1 * ((((c1 * (x .|. x)) + ((x .|. y) * ((- (x .|. y)) *' ))) + ((- (x .|. y)) * (y .|. x))) + ((- (x .|. y)) * ((- (x .|. y)) *' ))) by A6, Def13
.= c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) ;
then A7: ( Re (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) >= 0 & Im (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) = 0 ) by Def13;
Re (c1 * ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) = ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - ((Im c1) * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:24
.= ((Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) - (0 * (Im ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))))) by COMPLEX1:28
.= (Re c1) * (Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x)))) ;
then A8: ( ( Re c1 >= 0 & Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) >= 0 ) or ( Re c1 <= 0 & Re ((c1 * (x .|. x)) + ((- (x .|. y)) * (y .|. x))) <= 0 ) ) by A7, XREAL_1:134;
|.(y .|. y).| <> 0 by A3, COMPLEX1:131;
then A9: (Re (c1 * (x .|. x))) + (Re ((- (x .|. y)) * (y .|. x))) >= 0 by A4, A5, A8, COMPLEX1:19, COMPLEX1:29;
Re ((- (x .|. y)) * (y .|. x)) = Re (- ((x .|. y) * (y .|. x)))
.= - (Re ((x .|. y) * (y .|. x))) by COMPLEX1:34
.= - (Re ((x .|. y) * ((x .|. y) *' ))) by Def13 ;
then (Re (c1 * (x .|. x))) - (Re ((x .|. y) * ((x .|. y) *' ))) >= 0 by A9;
then A10: Re (c1 * (x .|. x)) >= (Re ((x .|. y) * ((x .|. y) *' ))) + 0 by XREAL_1:21;
A11: Re ((x .|. y) * ((x .|. y) *' )) = ((Re (x .|. y)) ^2 ) + ((Im (x .|. y)) ^2 ) by COMPLEX1:126;
( (Re (x .|. y)) ^2 >= 0 & (Im (x .|. y)) ^2 >= 0 ) by XREAL_1:65;
then A12: Re ((x .|. y) * ((x .|. y) *' )) >= 0 + 0 by A11, XREAL_1:9;
then abs (Re ((x .|. y) * ((x .|. y) *' ))) = Re ((x .|. y) * ((x .|. y) *' )) by ABSVALUE:def 1;
then A13: abs (Re (c1 * (x .|. x))) >= abs (Re ((x .|. y) * ((x .|. y) *' ))) by A10, A12, ABSVALUE:def 1;
( Im c1 = 0 & Im (x .|. x) = 0 ) by A4, A5, Def13, COMPLEX1:29;
then A14: Im (c1 * (x .|. x)) = ((Re c1) * 0 ) + ((Re (x .|. x)) * 0 ) by COMPLEX1:24;
then A15: ( Im (c1 * (x .|. x)) = 0 & Im ((x .|. y) * ((x .|. y) *' )) = 0 ) by COMPLEX1:126;
|.(c1 * (x .|. x)).| = abs (Re (c1 * (x .|. x))) by A14, COMPLEX1:136;
then |.(c1 * (x .|. x)).| >= |.((x .|. y) * ((x .|. y) *' )).| by A13, A15, COMPLEX1:136;
then |.(x .|. x).| * |.(y .|. y).| >= |.((x .|. y) * ((x .|. y) *' )).| by A6, COMPLEX1:151;
then |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.((x .|. y) *' ).| by COMPLEX1:151;
then A16: |.(x .|. x).| * |.(y .|. y).| >= |.(x .|. y).| * |.(x .|. y).| by COMPLEX1:139;
|.(x .|. y).| ^2 >= 0 by XREAL_1:65;
then A17: sqrt (|.(x .|. x).| * |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2 ) by A16, SQUARE_1:94;
( |.(x .|. x).| >= 0 & |.(y .|. y).| >= 0 & |.(x .|. y).| >= 0 ) by COMPLEX1:132;
then (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) >= sqrt (|.(x .|. y).| ^2 ) by A17, SQUARE_1:97;
hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by COMPLEX1:132, SQUARE_1:89; :: thesis: verum

end;

hence |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|) by A1; :: thesis: verum