let p1, p2, p3, p4 be Point of (TOP-REAL 2); 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); ( 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 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 )
and
A3:
( p1 <> p2 & p2 <> p3 )
and
A4:
p3 <> p4
; 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 )
consider f being Function of (TOP-REAL 2),(TOP-REAL 2), q1, q2, q3, q4 being Point of (TOP-REAL 2) such that
A5:
f is being_homeomorphism
and
A6:
for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.|
and
A7:
( q1 = f . p1 & q2 = f . p2 )
and
A8:
q3 = f . p3
and
A9:
q4 = f . p4
and
A10:
( q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 )
and
q4 `2 < 0
and
A11:
( LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
by A1, A2, Th65;
A12:
( dom f = the carrier of (TOP-REAL 2) & f is one-to-one )
by A5, FUNCT_2:def 1, TOPS_2:def 5;
then A13:
q3 <> q4
by A4, A8, A9, FUNCT_1:def 4;
( q1 <> q2 & q2 <> q3 )
by A3, A7, A8, A12, FUNCT_1:def 4;
then consider f2 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A14:
f2 is being_homeomorphism
and
A15:
for q being Point of (TOP-REAL 2) holds |.(f2 . q).| = |.q.|
and
A16:
( |[(- 1),0]| = f2 . q1 & |[0,1]| = f2 . q2 )
and
A17:
( |[1,0]| = f2 . q3 & |[0,(- 1)]| = f2 . q4 )
by A1, A10, A11, A13, Th66;
reconsider f3 = f2 * f as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A18:
f3 is being_homeomorphism
by A5, A14, TOPS_2:57;
A19:
dom f3 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then A20:
( f3 . p1 = |[(- 1),0]| & f3 . p2 = |[0,1]| )
by A7, A16, FUNCT_1:12;
A21:
for q being Point of (TOP-REAL 2) holds |.(f3 . q).| = |.q.|
( f3 . p3 = |[1,0]| & f3 . p4 = |[0,(- 1)]| )
by A8, A9, A17, A19, FUNCT_1:12;
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 A18, A21, A20; verum