let p, q be Point of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ & p in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & q in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p `2 >= q `2 & p `2 < 0 holds
(f . p) `2 >= (f . q) `2
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( f = Sq_Circ & p in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & q in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p `2 >= q `2 & p `2 < 0 implies (f . p) `2 >= (f . q) `2 )
assume A1: ( f = Sq_Circ & p in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & q in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p `2 >= q `2 & p `2 < 0 ) ; :: thesis: (f . p) `2 >= (f . q) `2
then A2: ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) by Th9;
A3: (p `2 ) ^2 >= 0 by XREAL_1:65;
A4: sqrt (1 + ((p `2 ) ^2 )) > 0 by A3, SQUARE_1:93;
A5: (q `2 ) ^2 >= 0 by XREAL_1:65;
A6: sqrt (1 + ((q `2 ) ^2 )) > 0 by A5, SQUARE_1:93;
A7: p `2 <= - (p `1 ) by A2;
p <> 0. (TOP-REAL 2) by A1, EUCLID:56, EUCLID:58;
then f . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A1, A2, A7, JGRAPH_3:def 1;
then A8: (f . p) `2 = (p `2 ) / (sqrt (1 + (((p `2 ) / (- 1)) ^2 ))) by A2, EUCLID:56
.= (p `2 ) / (sqrt (1 + ((p `2 ) ^2 ))) ;
A9: ( q `1 = - 1 & - 1 <= q `2 & q `2 <= 1 ) by A1, Th9;
then A10: q `2 <= - (q `1 ) ;
q <> 0. (TOP-REAL 2) by A1, EUCLID:56, EUCLID:58;
then f . q = |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| by A1, A9, A10, JGRAPH_3:def 1;
then A11: (f . q) `2 = (q `2 ) / (sqrt (1 + (((q `2 ) / (- 1)) ^2 ))) by A9, EUCLID:56
.= (q `2 ) / (sqrt (1 + ((q `2 ) ^2 ))) ;
(p `2 ) * (sqrt (1 + ((q `2 ) ^2 ))) >= (q `2 ) * (sqrt (1 + ((p `2 ) ^2 ))) by A1, Lm2;
then ((p `2 ) * (sqrt (1 + ((q `2 ) ^2 )))) / (sqrt (1 + ((q `2 ) ^2 ))) >= ((q `2 ) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((q `2 ) ^2 ))) by A6, XREAL_1:74;
then p `2 >= ((q `2 ) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((q `2 ) ^2 ))) by A6, XCMPLX_1:90;
then (p `2 ) / (sqrt (1 + ((p `2 ) ^2 ))) >= (((q `2 ) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((q `2 ) ^2 )))) / (sqrt (1 + ((p `2 ) ^2 ))) by A4, XREAL_1:74;
then (p `2 ) / (sqrt (1 + ((p `2 ) ^2 ))) >= (((q `2 ) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((q `2 ) ^2 ))) by XCMPLX_1:48;
hence (f . p) `2 >= (f . q) `2 by A4, A8, A11, XCMPLX_1:90; :: thesis: verum