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

proof

assume A2: x = H₁(X) ; :: thesis: abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
then A3: x .|. y = 0 by Th19;
sqrt (x .|. x) = 0 by A2, Def2, SQUARE_1:82;
hence abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by A3, ABSVALUE:7; :: thesis: verum

end;

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

proof

assume x <> H₁(X) ; :: thesis: abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y))
then A4: x .|. x <> 0 by Def2;
A5: x .|. x >= 0 by Def2;
A6: for t being real number holds (((x .|. x) * (t ^2 )) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0

proof

let t be real number ; :: thesis: (((x .|. x) * (t ^2 )) + ((2 * (x .|. y)) * t)) + (y .|. y) >= 0
reconsider t = t as Real by XREAL_0:def 1;
((t * x) + y) .|. ((t * x) + y) >= 0 by Def2;
then (((t * x) .|. (t * x)) + (2 * ((t * x) .|. y))) + (y .|. y) >= 0 by Th21;
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;

A7: (abs (x .|. y)) ^2 >= 0 by XREAL_1:65;
A8: y .|. y >= 0 by Def2;
delta (x .|. x),(2 * (x .|. y)),(y .|. y) <= 0 by A4, A5, A6, 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:79;
then (x .|. y) ^2 <= (x .|. x) * (y .|. y) by XREAL_1:52;
then (abs (x .|. y)) ^2 <= (x .|. x) * (y .|. y) by COMPLEX1:161;
then sqrt ((abs (x .|. y)) ^2 ) <= sqrt ((x .|. x) * (y .|. y)) by A7, SQUARE_1:94;
then abs (x .|. y) <= sqrt ((x .|. x) * (y .|. y)) by COMPLEX1:132, SQUARE_1:89;
hence abs (x .|. y) <= (sqrt (x .|. x)) * (sqrt (y .|. y)) by A5, A8, SQUARE_1:97; :: thesis: verum

end;

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