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 & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) 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 & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) 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 that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: ( LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 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 )
consider f being Function of (TOP-REAL 2),(TOP-REAL 2), q1, q2, q3, q4 being Point of (TOP-REAL 2) such that
A3: f is being_homeomorphism and
A4: for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| and
A5: ( q1 = f . p1 & q2 = f . p2 ) and
A6: ( q3 = f . p3 & q4 = f . p4 ) and
A7: ( q1 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A1, A2, Th62;
consider f2 being Function of (TOP-REAL 2),(TOP-REAL 2), q1b, q2b, q3b, q4b being Point of (TOP-REAL 2) such that
A8: f2 is being_homeomorphism and
A9: for q being Point of (TOP-REAL 2) holds |.(f2 . q).| = |.q.| and
A10: ( q1b = f2 . q1 & q2b = f2 . q2 ) and
A11: ( q3b = f2 . q3 & q4b = f2 . q4 ) and
A12: ( q1b `1 < 0 & q1b `2 < 0 & q2b `1 < 0 & q2b `2 < 0 & q3b `1 < 0 & q3b `2 < 0 & q4b `1 < 0 & q4b `2 < 0 & LE q1b,q2b,P & LE q2b,q3b,P & LE q3b,q4b,P ) by A1, A7, Th61;
reconsider f3 = f2 * f as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A13: f3 is being_homeomorphism by A3, A8, TOPS_2:57;
A14: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A15: ( f3 . p3 = q3b & f3 . p4 = q4b ) by A6, A11, FUNCT_1:13;
A16: 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 f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then f3 . q = f2 . (f . q) by FUNCT_1:13;
hence |.(f3 . q).| = |.(f . q).| by A9
.= |.q.| by A4 ;
:: thesis: verum

end;

( f3 . p1 = q1b & f3 . p2 = q2b ) by A5, A10, A14, FUNCT_1:13;
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 A12, A13, A16, A15; :: thesis: verum