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)]| holds
(f . p) `1 <= (f . q) `1
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)]| implies (f . p) `1 <= (f . q) `1 )
assume that
A1: f = Sq_Circ and
A2: p in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| and
A3: q in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| ; :: thesis: (f . p) `1 <= (f . q) `1
A4: p `1 = - 1 by A2, Th9;
A5: - 1 <= p `2 by A2, Th9;
A6: p `2 <= 1 by A2, Th9;
A7: q `2 = - 1 by A3, Th11;
A8: - 1 <= q `1 by A3, Th11;
A9: q `1 <= 1 by A3, Th11;
A10: p <> 0. (TOP-REAL 2) by A4, EUCLID:56, EUCLID:58;
A11: q <> 0. (TOP-REAL 2) by A7, EUCLID:56, EUCLID:58;
p `2 <= - (p `1 ) by A2, A4, Th9;
then f . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A1, A4, A5, A10, JGRAPH_3:def 1;
then A12: (f . p) `1 = (- 1) / (sqrt (1 + (((p `2 ) / (- 1)) ^2 ))) by A4, EUCLID:56
.= (- 1) / (sqrt (1 + ((p `2 ) ^2 ))) ;
(p `2 ) ^2 >= 0 by XREAL_1:65;
then A13: sqrt (1 + ((p `2 ) ^2 )) > 0 by SQUARE_1:93;
(q `1 ) ^2 >= 0 by XREAL_1:65;
then A14: sqrt (1 + ((q `1 ) ^2 )) > 0 by SQUARE_1:93;
q `1 <= - (q `2 ) by A3, A7, Th11;
then f . q = |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| by A1, A7, A8, A11, JGRAPH_3:14;
then A15: (f . q) `1 = (q `1 ) / (sqrt (1 + (((q `1 ) / (- 1)) ^2 ))) by A7, EUCLID:56
.= (q `1 ) / (sqrt (1 + ((q `1 ) ^2 ))) ;
- (sqrt (1 + ((q `1 ) ^2 ))) <= (q `1 ) * (sqrt (1 + ((p `2 ) ^2 ))) by A5, A6, A8, A9, SQUARE_1:125;
then ((- 1) * (sqrt (1 + ((q `1 ) ^2 )))) / (sqrt (1 + ((q `1 ) ^2 ))) <= ((q `1 ) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((q `1 ) ^2 ))) by A14, XREAL_1:74;
then - 1 <= ((q `1 ) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((q `1 ) ^2 ))) by A14, XCMPLX_1:90;
then - 1 <= ((q `1 ) / (sqrt (1 + ((q `1 ) ^2 )))) * (sqrt (1 + ((p `2 ) ^2 ))) by XCMPLX_1:75;
then (- 1) / (sqrt (1 + ((p `2 ) ^2 ))) <= (((q `1 ) / (sqrt (1 + ((q `1 ) ^2 )))) * (sqrt (1 + ((p `2 ) ^2 )))) / (sqrt (1 + ((p `2 ) ^2 ))) by A13, XREAL_1:74;
hence (f . p) `1 <= (f . q) `1 by A12, A13, A15, XCMPLX_1:90; :: thesis: verum