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
reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def 2;
consider x, y being Point of (TOP-REAL 2) such that
A1: x <> y and
A2: ( x in C & y in C ) by TOPREAL2:4;
A3: dist x,y > 0 by A1, JORDAN1K:22;
consider p1, p2 being Point of (TOP-REAL 2) such that
A4: p1,p2 realize-max-dist-in C by Th1;
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;
set arg = Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ));
reconsider qq = ((g . p2) `1 ) + (((g . p2) `2 ) * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
set h = Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> ))));
A5: Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) = Rotate ((2 * PI ) - (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) by Th6;
g . p1,g . p2 realize-max-dist-in g .: C by A4, Th3;
then A6: (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 Th4;
reconsider h0 = Rotate (- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) as isometric Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1, Th2;
A7: Rotate z,(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) = 0 by COMPLEX2:66;
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 Lm1, Lm4;
set F = h .: (g .: C);
set s1 = h . (g . p1);
set s2 = h . (g . p2);
g . p1 = |[((1 * (p1 `1 )) + (- (p1 `1 ))),((1 * (p1 `2 )) + (- (p1 `2 )))]| by JGRAPH_2:def 2
.= |[0 ,0 ]| ;
then A8: 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 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 A7, COMPLEX1:12, EUCLID:56 ;
Rotate qq,(- (Arg (((g . p2) `1 ) + (((g . p2) `2 ) * <i> )))) = |.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| + (0 * <i> ) by COMPLEX2:69;
then A9: 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 A10: (h . (g . p2)) `2 = 0 by EUCLID:56;
dist p1,p2 >= dist x,y by A4, A2, Def1;
then A11: p1 <> p2 by A3, TOPREAL6:102;

A12: now

dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A13: g . p1 <> g . p2 by A11, FUNCT_1:def 8;
assume A14: (h . (g . p2)) `1 = 0 ; :: thesis: contradiction
dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then h . (g . p1) <> h . (g . p2) by A13, FUNCT_1:def 8;
hence contradiction by A8, A9, A14, EUCLID:56; :: thesis: verum

end;

(h . (g . p2)) `1 = |.(((g . p2) `1 ) + (((g . p2) `2 ) * <i> )).| by A9, EUCLID:56;
then (h . (g . p2)) `1 >= 0 by COMPLEX1:132;
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 A12, JGRAPH_7:50;
set E = j .: (h .: (g .: C));
set r1 = j . (h . (g . p1));
set r2 = j . (h . (g . p2));
A15: 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 A12, XCMPLX_1:88
.= |[1,0 ]| by A10 ;
set f = j * (h * g);
h * g is being_homeomorphism by TOPS_2:71;
then j * (h * g) is being_homeomorphism by TOPS_2:71;
then reconsider f = j * (h * g) as Homeomorphism of TOP-REAL 2 by TOPGRP_1:def 4;
take f ; :: thesis: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in f .: C
(h * g) .: C = h .: (g .: C) by RELAT_1:159;
then A16: f .: C = j .: (h .: (g .: C)) by RELAT_1:159;
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 A8, EUCLID:56
.= |[(- 1),0 ]| by A8, EUCLID:56 ;
hence |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in f .: C by A5, A15, A16, A6, Th3; :: thesis: verum