let p1, p2 be Point of (); :: thesis: for P being non empty compact Subset of ()
for f being Function of (),() st P = circle (0,0,1) & f = Sq_Circ & p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p1 `2 >= 0 & LE p1,p2, rectangle ((- 1),1,(- 1),1) holds
LE f . p1,f . p2,P

let P be non empty compact Subset of (); :: thesis: for f being Function of (),() st P = circle (0,0,1) & f = Sq_Circ & p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p1 `2 >= 0 & LE p1,p2, rectangle ((- 1),1,(- 1),1) holds
LE f . p1,f . p2,P

let f be Function of (),(); :: thesis: ( P = circle (0,0,1) & f = Sq_Circ & p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p1 `2 >= 0 & LE p1,p2, rectangle ((- 1),1,(- 1),1) implies LE f . p1,f . p2,P )
set K = rectangle ((- 1),1,(- 1),1);
assume that
A1: P = circle (0,0,1) and
A2: f = Sq_Circ and
A3: p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) and
A4: p1 `2 >= 0 and
A5: LE p1,p2, rectangle ((- 1),1,(- 1),1) ; :: thesis: LE f . p1,f . p2,P
A6: rectangle ((- 1),1,(- 1),1) is being_simple_closed_curve by Th50;
A7: P = { p where p is Point of () : |.p.| = 1 } by ;
A8: p1 `1 = - 1 by ;
A9: p1 `2 <= 1 by ;
A10: p1 in rectangle ((- 1),1,(- 1),1) by ;
A11: p2 in rectangle ((- 1),1,(- 1),1) by ;
A12: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A13: dom f = the carrier of () by FUNCT_2:def 1;
then A14: f . p1 in P by ;
A15: f . p2 in P by ;
A16: p1 `1 = - 1 by ;
A17: (p1 `2) ^2 >= 0 by XREAL_1:63;
then A18: sqrt (1 + ((p1 `2) ^2)) > 0 by SQUARE_1:25;
A19: p1 `2 <= - (p1 `1) by A3, A8, Th1;
p1 <> 0. () by ;
then A20: f . p1 = |[((p1 `1) / (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))),((p1 `2) / (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))))]| by ;
then A21: (f . p1) `1 = (p1 `1) / (sqrt (1 + (((p1 `2) / (- 1)) ^2))) by
.= (p1 `1) / (sqrt (1 + ((p1 `2) ^2))) ;
A22: (f . p1) `2 = (p1 `2) / (sqrt (1 + (((p1 `2) / (- 1)) ^2))) by
.= (p1 `2) / (sqrt (1 + ((p1 `2) ^2))) ;
A23: (f . p1) `1 < 0 by ;
A24: (f . p1) `2 >= 0 by A4, A18, A22;
f . p1 in { p9 where p9 is Point of () : ( p9 in P & p9 `2 >= 0 ) } by A4, A14, A18, A22;
then A25: f . p1 in Upper_Arc P by ;
now :: thesis: ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 & LE f . p1,f . p2,P ) or ( p2 in LSeg (|[(- 1),1]|,|[1,1]|) & LE f . p1,f . p2,P ) or ( p2 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p1,f . p2,P ) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| & LE f . p1,f . p2,P ) )
per cases ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 ) or p2 in LSeg (|[(- 1),1]|,|[1,1]|) or p2 in LSeg (|[1,1]|,|[1,(- 1)]|) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| ) ) by A3, A5, Th64;
case A26: ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 ) ; :: thesis: LE f . p1,f . p2,P
A27: (p2 `2) ^2 >= 0 by XREAL_1:63;
then A28: sqrt (1 + ((p2 `2) ^2)) > 0 by SQUARE_1:25;
A29: p2 `1 = - 1 by ;
A30: - 1 <= p2 `2 by ;
A31: p2 `2 <= - (p2 `1) by ;
p2 <> 0. () by ;
then A32: f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| by ;
then A33: (f . p2) `1 = (p2 `1) / (sqrt (1 + (((p2 `2) / (- 1)) ^2))) by
.= (p2 `1) / (sqrt (1 + ((p2 `2) ^2))) ;
A34: (f . p2) `2 = (p2 `2) / (sqrt (1 + (((p2 `2) / (- 1)) ^2))) by
.= (p2 `2) / (sqrt (1 + ((p2 `2) ^2))) ;
A35: (f . p2) `1 < 0 by ;
(p1 `2) * (sqrt (1 + ((p2 `2) ^2))) <= (p2 `2) * (sqrt (1 + ((p1 `2) ^2))) by A4, A26, Lm3;
then ((p1 `2) * (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2))) <= ((p2 `2) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2))) by ;
then p1 `2 <= ((p2 `2) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2))) by ;
then (p1 `2) / (sqrt (1 + ((p1 `2) ^2))) <= (((p2 `2) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p1 `2) ^2))) by ;
then (p1 `2) / (sqrt (1 + ((p1 `2) ^2))) <= (((p2 `2) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2))) by XCMPLX_1:48;
then (f . p1) `2 <= (f . p2) `2 by ;
hence LE f . p1,f . p2,P by ; :: thesis: verum
end;
case A36: p2 in LSeg (|[(- 1),1]|,|[1,1]|) ; :: thesis: LE f . p1,f . p2,P
then A37: p2 `2 = 1 by Th3;
A38: - 1 <= p2 `1 by ;
A39: p2 `1 <= 1 by ;
(p2 `1) ^2 >= 0 by XREAL_1:63;
then A40: sqrt (1 + ((p2 `1) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. () by ;
then A41: f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| by ;
then A42: (f . p2) `1 = (p2 `1) / (sqrt (1 + ((p2 `1) ^2))) by ;
A43: (f . p2) `2 >= 0 by ;
- (sqrt (1 + ((p2 `1) ^2))) <= (p2 `1) * (sqrt (1 + ((p1 `2) ^2))) by ;
then ((p1 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p2 `1) ^2))) <= ((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `1) ^2))) by ;
then p1 `1 <= ((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `1) ^2))) by ;
then (p1 `1) / (sqrt (1 + ((p1 `2) ^2))) <= (((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p1 `2) ^2))) by ;
then (p1 `1) / (sqrt (1 + ((p1 `2) ^2))) <= (((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `1) ^2))) by XCMPLX_1:48;
then (f . p1) `1 <= (f . p2) `1 by ;
hence LE f . p1,f . p2,P by ; :: thesis: verum
end;
case A44: p2 in LSeg (|[1,1]|,|[1,(- 1)]|) ; :: thesis: LE f . p1,f . p2,P
then A45: p2 `1 = 1 by Th1;
A46: - 1 <= p2 `2 by ;
A47: p2 `2 <= 1 by ;
(p2 `2) ^2 >= 0 by XREAL_1:63;
then A48: sqrt (1 + ((p2 `2) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. () by ;
then f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| by ;
then A49: (f . p2) `1 = (p2 `1) / (sqrt (1 + ((p2 `2) ^2))) by ;
(p1 `1) / (sqrt (1 + ((p1 `2) ^2))) <= (((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p1 `2) ^2))) by ;
then (p1 `1) / (sqrt (1 + ((p1 `2) ^2))) <= (((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2))) by XCMPLX_1:48;
then A50: (f . p1) `1 <= (f . p2) `1 by ;
now :: thesis: ( ( (f . p2) `2 >= 0 & LE f . p1,f . p2,P ) or ( (f . p2) `2 < 0 & LE f . p1,f . p2,P ) )
per cases ( (f . p2) `2 >= 0 or (f . p2) `2 < 0 ) ;
case (f . p2) `2 >= 0 ; :: thesis: LE f . p1,f . p2,P
hence LE f . p1,f . p2,P by ; :: thesis: verum
end;
case A51: (f . p2) `2 < 0 ; :: thesis: LE f . p1,f . p2,P
then f . p2 in { p9 where p9 is Point of () : ( p9 in P & p9 `2 <= 0 ) } by A15;
then A52: f . p2 in Lower_Arc P by ;
W-min P = |[(- 1),0]| by ;
then f . p2 <> W-min P by ;
hence LE f . p1,f . p2,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p1,f . p2,P ; :: thesis: verum
end;
case A53: ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| ) ; :: thesis: LE f . p1,f . p2,P
then A54: p2 `2 = - 1 by Th3;
A55: - 1 <= p2 `1 by ;
A56: (p2 `1) ^2 >= 0 by XREAL_1:63;
A57: p2 `1 <= - (p2 `2) by ;
p2 <> 0. () by ;
then f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| by ;
then (f . p2) `2 = (p2 `2) / (sqrt (1 + (((p2 `1) / (- 1)) ^2))) by
.= (p2 `2) / (sqrt (1 + ((p2 `1) ^2))) ;
then A58: (f . p2) `2 < 0 by ;
then f . p2 in { p9 where p9 is Point of () : ( p9 in P & p9 `2 <= 0 ) } by A15;
then A59: f . p2 in Lower_Arc P by ;
W-min P = |[(- 1),0]| by ;
then f . p2 <> W-min P by ;
hence LE f . p1,f . p2,P by ; :: thesis: verum
end;
end;
end;
hence LE f . p1,f . p2,P ; :: thesis: verum