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 <> p2 & p2 <> p3 & p3 <> p4 holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0 ]| = f . p1 & |[0 ,1]| = f . p2 & |[1,0 ]| = f . p3 & |[0 ,(- 1)]| = f . p4 )
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 <> p2 & p2 <> p3 & p3 <> p4 implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0 ]| = f . p1 & |[0 ,1]| = f . p2 & |[1,0 ]| = f . p3 & |[0 ,(- 1)]| = f . p4 ) )
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 & p1 <> p2 & p2 <> p3 & p3 <> p4 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0 ]| = f . p1 & |[0 ,1]| = f . p2 & |[1,0 ]| = f . p3 & |[0 ,(- 1)]| = f . p4 )
then consider f being Function of (TOP-REAL 2),(TOP-REAL 2), q1, q2, q3, q4 being Point of (TOP-REAL 2) such that
A2: ( 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 Th68;
A3: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A4: f is one-to-one by A2, TOPS_2:def 5;
then A5: q1 <> q2 by A1, A2, A3, FUNCT_1:def 8;
A6: q2 <> q3 by A1, A2, A3, A4, FUNCT_1:def 8;
q3 <> q4 by A1, A2, A3, A4, FUNCT_1:def 8;
then consider f2 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A7: ( f2 is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f2 . q).| = |.q.| ) & |[(- 1),0 ]| = f2 . q1 & |[0 ,1]| = f2 . q2 & |[1,0 ]| = f2 . q3 & |[0 ,(- 1)]| = f2 . q4 ) by A1, A2, A5, A6, Th69;
reconsider f3 = f2 * f as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A8: f3 is being_homeomorphism by A2, A7, TOPS_2:71;
A9: dom f3 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A10: 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.|
|.(f3 . q).| = |.(f2 . (f . q)).| by A9, FUNCT_1:22
.= |.(f . q).| by A7
.= |.q.| by A2 ;
hence |.(f3 . q).| = |.q.| ; :: thesis: verum

end;

A11: f3 . p1 = |[(- 1),0 ]| by A2, A7, A9, FUNCT_1:22;
A12: f3 . p2 = |[0 ,1]| by A2, A7, A9, FUNCT_1:22;
A13: f3 . p3 = |[1,0 ]| by A2, A7, A9, FUNCT_1:22;
f3 . p4 = |[0 ,(- 1)]| by A2, A7, A9, FUNCT_1:22;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0 ]| = f . p1 & |[0 ,1]| = f . p2 & |[1,0 ]| = f . p3 & |[0 ,(- 1)]| = f . p4 ) by A8, A10, A11, A12, A13; :: thesis: verum