let X be RealUnitarySpace; :: 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: ( x <> H₁(X) implies |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y)) )

proof

A2: for t being Real holds (((x .|. x) * (t ^2)) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0

proof

let t be Real; :: thesis: (((x .|. x) * (t ^2)) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0
reconsider t = t as Real ;
((t * x) + y) .|. ((t * x) + y) >= 0 by Def2;
then (((t * x) .|. (t * x)) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Th16;
then ((t * (x .|. (t * x))) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Def2;
then ((t * (t * (x .|. x))) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Def2;
then (((x .|. x) * (t ^2)) + (2 * ((x .|. y) * t))) + (y .|. y) >= 0 by Def2;
hence (((x .|. x) * (t ^2)) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0 ; :: thesis: verum

end;

A3: x .|. x >= 0 by Def2;
assume x <> H₁(X) ; :: thesis: |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y))
then x .|. x <> 0 by Def2;
then delta ((x .|. x),(2 * (x .|. y)),(y .|. y)) <= 0 by A3, A2, QUIN_1:10;
then ((2 * (x .|. y)) ^2) - ((4 * (x .|. x)) * (y .|. y)) <= 0 by QUIN_1:def 1;
then 4 * (((x .|. y) ^2) - ((x .|. x) * (y .|. y))) <= 0 ;
then ((x .|. y) ^2) - ((x .|. x) * (y .|. y)) <= 0 / 4 by XREAL_1:77;
then (x .|. y) ^2 <= (x .|. x) * (y .|. y) by XREAL_1:50;
then ( |.(x .|. y).| ^2 >= 0 & |.(x .|. y).| ^2 <= (x .|. x) * (y .|. y) ) by COMPLEX1:75, XREAL_1:63;
then sqrt (|.(x .|. y).| ^2) <= sqrt ((x .|. x) * (y .|. y)) by SQUARE_1:26;
then A4: |.(x .|. y).| <= sqrt ((x .|. x) * (y .|. y)) by COMPLEX1:46, SQUARE_1:22;
y .|. y >= 0 by Def2;
hence |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by A3, A4, SQUARE_1:29; :: thesis: verum

end;

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

proof

assume x = H₁(X) ; :: thesis: |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y))
then ( x .|. y = 0 & sqrt (x .|. x) = 0 ) by Th14, SQUARE_1:17;
hence |.(x .|. y).| <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by ABSVALUE:2; :: thesis: verum

end;

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