let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) )
assume A1: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
then A2: P is being_simple_closed_curve by JGRAPH_3:36;
then A3: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
A4: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p3 in P & p4 in P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ) by A1, A2, JORDAN7:5;
then consider p44 being Point of (TOP-REAL 2) such that
A5: ( p44 = p4 & |.p44.| = 1 ) ;
A6: ( - 1 <= p4 `1 & p4 `1 <= 1 ) by A5, Th3;
A7: Lower_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 <= 0 ) } by A1, Th38;
A8: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th37;
A9: W-min P = |[(- 1),0 ]| by A1, Th32;
then A10: ( (W-min P) `1 = - 1 & (W-min P) `2 = 0 ) by EUCLID:56;
now
per cases ( p4 `1 = - 1 or p4 `1 <> - 1 ) ;
case A11: p4 `1 = - 1 ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
1 ^2 = ((p4 `1 ) ^2 ) + ((p4 `2 ) ^2 ) by A5, JGRAPH_3:10
.= ((p4 `2 ) ^2 ) + 1 by A11 ;
then A12: p4 `2 = 0 by XCMPLX_1:6;
then A13: p4 in Upper_Arc P by A4, A8;
A14: p4 = W-min P by A9, A11, A12, EUCLID:57;
LE p1,p3,P by A1, JGRAPH_3:36, JORDAN6:73;
then LE p1,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
then A18: p4 = p1 by A1, A15, JGRAPH_3:36, JORDAN6:72;
A19: LE p4,p2,P by A1, A15, JGRAPH_3:36, JORDAN6:73;
LE p2,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
then A20: p2 = p4 by A1, A19, JGRAPH_3:36, JORDAN6:72;
LE p4,p3,P by A1, A19, JGRAPH_3:36, JORDAN6:73;
then p3 = p4 by A1, JGRAPH_3:36, JORDAN6:72;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A1, A11, A12, A18, A20, Th62; :: thesis: verum
end;
case A21: p4 `1 <> - 1 ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
then p4 `1 > - 1 by A6, XXREAL_0:1;
then consider r being real number such that
A22: ( - 1 < r & r < p4 `1 ) by XREAL_1:7;
reconsider r1 = r as Real by XREAL_0:def 1;
A23: ( - 1 < r1 & r1 < 1 ) by A6, A22, XXREAL_0:2;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A24: ( f1 = r1 -FanMorphS & f1 is being_homeomorphism ) by JGRAPH_4:143;
set q11 = f1 . p1;
set q22 = f1 . p2;
set q33 = f1 . p3;
set q44 = f1 . p4;
now
per cases ( p4 `1 > 0 or p4 `2 >= 0 or ( p4 `1 <= 0 & p4 `2 < 0 ) ) ;
case A25: ( p4 `1 > 0 or p4 `2 >= 0 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
then A26: ( p3 `1 >= 0 or p3 `2 >= 0 ) by A1, Th52;
then A27: ( p2 `1 >= 0 or p2 `2 >= 0 ) by A1, Th52;
then A28: ( p1 `1 >= 0 or p1 `2 >= 0 ) by A1, Th52;
now
assume A29: ( p4 `2 = 0 & p4 `1 <= 0 ) ; :: thesis: contradiction
1 ^2 = ((p4 `1 ) ^2 ) + ((p4 `2 ) ^2 ) by A5, JGRAPH_3:10
.= (p4 `1 ) ^2 by A29 ;
hence contradiction by A21, A29, SQUARE_1:109; :: thesis: verum
end;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A1, A25, A26, A27, A28, Th66; :: thesis: verum
end;
case A30: ( p4 `1 <= 0 & p4 `2 < 0 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
(p4 `1 ) / |.p4.| > r1 by A5, A22;
then A31: ( (f1 . p4) `1 > 0 & (f1 . p4) `2 < 0 ) by A22, A24, A30, Th29;
A32: LE f1 . p3,f1 . p4,P by A1, A23, A24, Th61;
A33: LE f1 . p2,f1 . p3,P by A1, A23, A24, Th61;
then A34: LE f1 . p2,f1 . p4,P by A1, A32, JGRAPH_3:36, JORDAN6:73;
A35: LE f1 . p1,f1 . p2,P by A1, A23, A24, Th61;
W-min P = |[(- 1),0 ]| by A1, Th32;
then A36: (W-min P) `2 = 0 by EUCLID:56;
A37: now
per cases ( (f1 . p3) `2 >= 0 or (f1 . p3) `2 < 0 ) ;
case (f1 . p3) `2 >= 0 ; :: thesis: ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 )
hence ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 ) ; :: thesis: verum
end;
case (f1 . p3) `2 < 0 ; :: thesis: ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 )
thus ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 ) by A1, A31, A32, A36, Th51; :: thesis: verum
end;
end;
end;
A38: now
per cases ( (f1 . p2) `2 >= 0 or (f1 . p2) `2 < 0 ) ;
case (f1 . p2) `2 >= 0 ; :: thesis: ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 )
hence ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 ) ; :: thesis: verum
end;
case (f1 . p2) `2 < 0 ; :: thesis: ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 )
thus ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 ) by A1, A2, A31, A32, A33, A36, Th51, JORDAN6:73; :: thesis: verum
end;
end;
end;
now
per cases ( (f1 . p1) `2 >= 0 or (f1 . p1) `2 < 0 ) ;
case (f1 . p1) `2 >= 0 ; :: thesis: ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 )
hence ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 ) ; :: thesis: verum
end;
case (f1 . p1) `2 < 0 ; :: thesis: ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 )
thus ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 ) by A1, A2, A31, A34, A35, A36, Th51, JORDAN6:73; :: thesis: verum
end;
end;
end;
then consider f2 being Function of (TOP-REAL 2),(TOP-REAL 2), q81, q82, q83, q84 being Point of (TOP-REAL 2) such that
A39: ( f2 is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f2 . q).| = |.q.| ) & q81 = f2 . (f1 . p1) & q82 = f2 . (f1 . p2) & q83 = f2 . (f1 . p3) & q84 = f2 . (f1 . p4) & q81 `1 < 0 & q81 `2 < 0 & q82 `1 < 0 & q82 `2 < 0 & q83 `1 < 0 & q83 `2 < 0 & q84 `1 < 0 & q84 `2 < 0 & LE q81,q82,P & LE q82,q83,P & LE q83,q84,P ) by A1, A31, A32, A33, A35, A37, A38, Th66;
reconsider f3 = f2 * f1 as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A40: f3 is being_homeomorphism by A24, A39, TOPS_2:71;
A41: for q being Point of (TOP-REAL 2) holds |.(f3 . q).| = |.q.|
proof
let q be Point of (TOP-REAL 2); :: thesis: |.(f3 . q).| = |.q.|
dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then f3 . q = f2 . (f1 . q) by FUNCT_1:23;
hence |.(f3 . q).| = |.(f1 . q).| by A39
.= |.q.| by A24, JGRAPH_4:135 ;
:: thesis: verum
end;
A42: dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A43: f3 . p1 = q81 by A39, FUNCT_1:23;
A44: f3 . p2 = q82 by A39, A42, FUNCT_1:23;
A45: f3 . p3 = q83 by A39, A42, FUNCT_1:23;
f3 . p4 = q84 by A39, A42, FUNCT_1:23;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A39, A40, A41, A43, A44, A45; :: thesis: verum
end;
end;
end;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ; :: thesis: verum
end;
end;
end;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ; :: thesis: verum