let p, q be Point of (TOP-REAL 2); 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); ( 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)]|)
; (f . p) `1 <= (f . q) `1
A4:
p `1 = - 1
by A2, Th1;
A5:
- 1 <= p `2
by A2, Th1;
A6:
p `2 <= 1
by A2, Th1;
A7:
q `2 = - 1
by A3, Th3;
A8:
- 1 <= q `1
by A3, Th3;
A9:
q `1 <= 1
by A3, Th3;
A10:
p <> 0. (TOP-REAL 2)
by A4, EUCLID:52, EUCLID:54;
A11:
q <> 0. (TOP-REAL 2)
by A7, EUCLID:52, EUCLID:54;
p `2 <= - (p `1)
by A2, A4, Th1;
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:52
.=
(- 1) / (sqrt (1 + ((p `2) ^2)))
;
(p `2) ^2 >= 0
by XREAL_1:63;
then A13:
sqrt (1 + ((p `2) ^2)) > 0
by SQUARE_1:25;
(q `1) ^2 >= 0
by XREAL_1:63;
then A14:
sqrt (1 + ((q `1) ^2)) > 0
by SQUARE_1:25;
q `1 <= - (q `2)
by A3, A7, Th3;
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:4;
then A15: (f . q) `1 =
(q `1) / (sqrt (1 + (((q `1) / (- 1)) ^2)))
by A7, EUCLID:52
.=
(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:55;
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:72;
then
- 1 <= ((q `1) * (sqrt (1 + ((p `2) ^2)))) / (sqrt (1 + ((q `1) ^2)))
by A14, XCMPLX_1:89;
then
- 1 <= ((q `1) / (sqrt (1 + ((q `1) ^2)))) * (sqrt (1 + ((p `2) ^2)))
by XCMPLX_1:74;
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:72;
hence
(f . p) `1 <= (f . q) `1
by A12, A13, A15, XCMPLX_1:89; verum