let C be Simple_closed_curve; :: thesis: ex f being Homeomorphism of TOP-REAL 2 st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in f .: C
consider p1, p2 being Point of (TOP-REAL 2) such that
A1: p1,p2 realize-max-dist-in C by Th1;
consider x, y being Point of (TOP-REAL 2) such that
A2: ( x <> y & x in C & y in C ) by TOPREAL2:4;
( dist x,y > 0 & dist p1,p2 >= dist x,y ) by A1, A2, Def1, JORDAN1K:22;
then A3: p1 <> p2 by TOPREAL6:102;
reconsider g = AffineMap 1,(- (p1 `1 )),1,(- (p1 `2 )) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by JGRAPH_7:50;
set D = g .: C;
set q1 = g . p1;
set q2 = g . p2;
A4: g . p1,g . p2 realize-max-dist-in g .: C by A1, Th3;
A5: g . p1 = |[((1 * (p1 `1 )) + (- (p1 `1 ))),((1 * (p1 `2 )) + (- (p1 `2 )))]| by JGRAPH_2:def 2
.= |[0 ,0 ]| ;
set arg = Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ));
set h = Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))));
A13: Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) = Rotate ((2 * PI ) - (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) by Th6;
reconsider h0 = Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) as isometric Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Th2, XX;
h0 is being_homeomorphism ;
then reconsider h = Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by XX, LmX;
set F = h .: (g .: C);
set s1 = h . (g . p1);
set s2 = h . (g . p2);
reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def 2;
A14: Rotate z,(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) = 0 by COMPLEX2:66;
A15: h . (g . p1) = |[(Re (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))))),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))))]| by A5, Def3
.= |[(Re (Rotate (0 + ((|[0 ,0 ]| `2 ) * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))))),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))))]| by EUCLID:56
.= |[(Re (Rotate (0 + (0 * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))))),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))))]| by EUCLID:56
.= |[(Re (Rotate (0 + (0 * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))))),(Im (Rotate (0 + ((|[0 ,0 ]| `2 ) * <i> )),(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))))]| by EUCLID:56
.= |[0 ,0 ]| by A14, COMPLEX1:12, EUCLID:56 ;
reconsider qq = ((g . p2) `1 ) + (((g . p2) `2 ) * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
Rotate qq,(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) = |.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| + (0 * <i> ) by COMPLEX2:69;
then A16: h . (g . p2) = |[(Re (|.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| + (0 * <i> ))),(Im (|.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| + (0 * <i> )))]| by Def3
.= |[|.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).|,(Im (|.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| + (0 * <i> )))]| by COMPLEX1:28
.= |[|.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).|,0 ]| by COMPLEX1:28 ;
then A17: ( (h . (g . p2)) `1 = |.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| & (h . (g . p2)) `2 = 0 ) by EUCLID:56;
then A18: ( (h . (g . p2)) `1 >= 0 & (h . (g . p2)) `2 = 0 ) by COMPLEX1:132;

A19: now

assume A20: (h . (g . p2)) `1 = 0 ; :: thesis: contradiction
dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A21: g . p1 <> g . p2 by A3, FUNCT_1:def 8;
dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then h . (g . p1) <> h . (g . p2) by A21, FUNCT_1:def 8;
hence contradiction by A15, A16, A20, EUCLID:56; :: thesis: verum

end;

then reconsider j = AffineMap (2 / ((h . (g . p2)) `1 )),(- 1),(2 / ((h . (g . p2)) `1 )),0 as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by A18, JGRAPH_7:50;
set E = j .: (h .: (g .: C));
set r1 = j . (h . (g . p1));
set r2 = j . (h . (g . p2));
set f = j * (h * g);
j * (h * g) is Homeomorphism of TOP-REAL 2

proof

h * g is being_homeomorphism by TOPS_2:71;
hence j * (h * g) is being_homeomorphism by TOPS_2:71; :: according to TOPGRP_1:def 4 :: thesis: verum

end;

then reconsider f = j * (h * g) as Homeomorphism of TOP-REAL 2 ;
take f ; :: thesis: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in f .: C
A22: j . (h . (g . p1)) = |[(((2 / ((h . (g . p2)) `1 )) * ((h . (g . p1)) `1 )) + (- 1)),(((2 / ((h . (g . p2)) `1 )) * ((h . (g . p1)) `2 )) + 0 )]| by JGRAPH_2:def 2
.= |[(((2 / ((h . (g . p2)) `1 )) * 0 ) + (- 1)),(((2 / ((h . (g . p2)) `1 )) * ((h . (g . p1)) `2 )) + 0 )]| by A15, EUCLID:56
.= |[(- 1),0 ]| by A15, EUCLID:56 ;
A23: j . (h . (g . p2)) = |[(((2 / ((h . (g . p2)) `1 )) * ((h . (g . p2)) `1 )) + (- 1)),(((2 / ((h . (g . p2)) `1 )) * ((h . (g . p2)) `2 )) + 0 )]| by JGRAPH_2:def 2
.= |[(2 + (- 1)),(((2 / ((h . (g . p2)) `1 )) * ((h . (g . p2)) `2 )) + 0 )]| by A19, XCMPLX_1:88
.= |[1,0 ]| by A17 ;
(h * g) .: C = h .: (g .: C) by RELAT_1:159;
then A24: f .: C = j .: (h .: (g .: C)) by RELAT_1:159;
(Rotate ((2 * PI ) - (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))) . (g . p1),(Rotate ((2 * PI ) - (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))) . (g . p2) realize-max-dist-in (Rotate ((2 * PI ) - (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))))) .: (g .: C) by A4, Th4;
hence |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in f .: C by A13, A22, A23, A24, Th3; :: thesis: verum