let p, q be Point of (); :: thesis: for f being Function of (),() 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 (),(); :: 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 that
A1: f = Sq_Circ and
A2: p in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) and
A3: q in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) and
A4: p `2 >= q `2 and
A5: p `2 < 0 ; :: thesis: (f . p) `2 >= (f . q) `2
A6: p `1 = - 1 by ;
A7: - 1 <= p `2 by ;
(p `2) ^2 >= 0 by XREAL_1:63;
then A8: sqrt (1 + ((p `2) ^2)) > 0 by SQUARE_1:25;
(q `2) ^2 >= 0 by XREAL_1:63;
then A9: sqrt (1 + ((q `2) ^2)) > 0 by SQUARE_1:25;
A10: p `2 <= - (p `1) by A5, A6;
p <> 0. () by ;
then f . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by ;
then A11: (f . p) `2 = (p `2) / (sqrt (1 + (((p `2) / (- 1)) ^2))) by
.= (p `2) / (sqrt (1 + ((p `2) ^2))) ;
A12: q `1 = - 1 by ;
A13: - 1 <= q `2 by ;
A14: q `2 <= - (q `1) by A4, A5, A12;
q <> 0. () by ;
then f . q = |[((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))),((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2))))]| by ;
then A15: (f . q) `2 = (q `2) / (sqrt (1 + (((q `2) / (- 1)) ^2))) by
.= (q `2) / (sqrt (1 + ((q `2) ^2))) ;
(p `2) * (sqrt (1 + ((q `2) ^2))) >= (q `2) * (sqrt (1 + ((p `2) ^2))) by A4, A5, 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 ;
then p `2 >= ((q `2) * (sqrt (1 + ((p `2) ^2)))) / (sqrt (1 + ((q `2) ^2))) by ;
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 ;
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 ; :: thesis: verum