let sn be Real; :: thesis: ( - 1 < sn & sn < 1 implies ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphW & h is continuous ) )
assume A1: ( - 1 < sn & sn < 1 ) ; :: thesis: ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphW & h is continuous )
reconsider f = sn -FanMorphW as Function of (TOP-REAL 2),(TOP-REAL 2) ;
reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:19;
A2: f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) by Th23, JGRAPH_2:11;
A3: D ` = {(0. (TOP-REAL 2))} by JGRAPH_3:30;
A4: for p being Point of ((TOP-REAL 2) | D) holds f . p <> f . (0. (TOP-REAL 2))

proof

let p be Point of ((TOP-REAL 2) | D); :: thesis: f . p <> f . (0. (TOP-REAL 2))
A5: [#] ((TOP-REAL 2) | D) = D by PRE_TOPC:def 10;
then A6: ( p in the carrier of (TOP-REAL 2) & not p in {(0. (TOP-REAL 2))} ) by XBOOLE_0:def 5;
reconsider q = p as Point of (TOP-REAL 2) by A5, XBOOLE_0:def 5;
A7: p <> 0. (TOP-REAL 2) by A6, TARSKI:def 1;

per cases ( ( (q `2 ) / |.q.| >= sn & q `1 <= 0 ) or ( (q `2 ) / |.q.| < sn & q `1 <= 0 ) or q `1 > 0 ) ;

suppose A8: ( (q `2 ) / |.q.| >= sn & q `1 <= 0 ) ; :: thesis: f . p <> f . (0. (TOP-REAL 2))

set q9 = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]|;
A9: ( |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `1 = |.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))) & |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)) ) by EUCLID:56;

now

assume A10: |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
A11: |.q.| <> 0 ^2 by A7, TOPRNS_1:25;
then - (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) = - (sqrt (1 - 0 )) by A9, A10, JGRAPH_2:11, XCMPLX_1:6
.= - 1 by SQUARE_1:83 ;
hence contradiction by A9, A10, A11, JGRAPH_2:11, XCMPLX_1:6; :: thesis: verum

end;

hence f . p <> f . (0. (TOP-REAL 2)) by A1, A2, A7, A8, Th25; :: thesis: verum

end;

suppose A12: ( (q `2 ) / |.q.| < sn & q `1 <= 0 ) ; :: thesis: f . p <> f . (0. (TOP-REAL 2))

set q9 = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]|;
A13: ( |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `1 = |.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))) & |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)) ) by EUCLID:56;

now

assume A14: |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
A15: |.q.| <> 0 ^2 by A7, TOPRNS_1:25;
then - (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) = - (sqrt (1 - 0 )) by A13, A14, JGRAPH_2:11, XCMPLX_1:6
.= - 1 by SQUARE_1:83 ;
hence contradiction by A13, A14, A15, JGRAPH_2:11, XCMPLX_1:6; :: thesis: verum

end;

hence f . p <> f . (0. (TOP-REAL 2)) by A1, A2, A7, A12, Th25; :: thesis: verum

end;

suppose q `1 > 0 ; :: thesis: f . p <> f . (0. (TOP-REAL 2))

then f . p = p by Th23;
hence f . p <> f . (0. (TOP-REAL 2)) by A7, Th23, JGRAPH_2:11; :: thesis: verum

end;

end;

end;

A16: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphW ) | D & h is continuous ) by A1, A3, Th43;
for V being Subset of (TOP-REAL 2) st f . (0. (TOP-REAL 2)) in V & V is open holds
ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )

proof

let V be Subset of (TOP-REAL 2); :: thesis: ( f . (0. (TOP-REAL 2)) in V & V is open implies ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) )
assume A17: ( f . (0. (TOP-REAL 2)) in V & V is open ) ; :: thesis: ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V )
reconsider u0 = 0. (TOP-REAL 2) as Point of (Euclid 2) by EUCLID:71;
reconsider VV = V as Subset of (TopSpaceMetr (Euclid 2)) by XX;
VV is open by A17, XX, PRE_TOPC:60;
then consider r being real number such that
A18: ( r > 0 & Ball u0,r c= V ) by A2, A17, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider W1 = Ball u0,r as Subset of (TOP-REAL 2) ;
A19: u0 in W1 by A18, GOBOARD6:4;
A20: W1 is open by GOBOARD6:6;
f .: W1 c= W1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: W1 or z in W1 )
assume z in f .: W1 ; :: thesis: z in W1
then consider y being set such that
A21: ( y in dom f & y in W1 & z = f . y ) by FUNCT_1:def 12;
reconsider q = y as Point of (TOP-REAL 2) by A21;
reconsider qy = q as Point of (Euclid 2) by EUCLID:71;
z in rng f by A21, FUNCT_1:def 5;
then reconsider qz = z as Point of (TOP-REAL 2) ;
reconsider pz = qz as Point of (Euclid 2) by EUCLID:71;
dist u0,qy < r by A21, METRIC_1:12;
then A22: |.((0. (TOP-REAL 2)) - q).| < r by JGRAPH_1:45;

per cases ( q `1 >= 0 or ( q <> 0. (TOP-REAL 2) & (q `2 ) / |.q.| >= sn & q `1 <= 0 ) or ( q <> 0. (TOP-REAL 2) & (q `2 ) / |.q.| < sn & q `1 <= 0 ) ) by JGRAPH_2:11;

suppose q `1 >= 0 ; :: thesis: z in W1

hence z in W1 by A21, Th23; :: thesis: verum

end;

suppose A23: ( q <> 0. (TOP-REAL 2) & (q `2 ) / |.q.| >= sn & q `1 <= 0 ) ; :: thesis: z in W1

then A24: (sn -FanMorphW ) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| by A1, Th25;
|.q.| <> 0 by A23, TOPRNS_1:25;
then A25: |.q.| ^2 > 0 by SQUARE_1:74;
A26: 1 - sn > 0 by A1, XREAL_1:151;
A27: ( qz `1 = |.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))) & qz `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)) ) by A21, A24, EUCLID:56;
A28: ((q `2 ) / |.q.|) - sn >= 0 by A23, XREAL_1:50;
A29: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
0 <= (q `1 ) ^2 by XREAL_1:65;
then 0 + ((q `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by XREAL_1:9;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 ) by A29, XREAL_1:74;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= 1 by A25, XCMPLX_1:60;
then ((q `2 ) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (q `2 ) / |.q.| by SQUARE_1:121;
then A30: 1 - sn >= ((q `2 ) / |.q.|) - sn by XREAL_1:11;
A31: - (1 - sn) <= - 0 by A26;
- (1 - sn) <= - (((q `2 ) / |.q.|) - sn) by A30, XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) by A26, XREAL_1:74;
then A32: - 1 <= (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) by A26, XCMPLX_1:198;
- (- (1 - sn)) >= - (((q `2 ) / |.q.|) - sn) by A28, A31, XREAL_1:26;
then (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) <= 1 by A26, XREAL_1:187;
then ((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A32, SQUARE_1:119;
then 1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 ) >= 0 by XREAL_1:50;
then A33: 1 - ((- ((((q `2 ) / |.q.|) - sn) / (1 - sn))) ^2 ) >= 0 by XCMPLX_1:188;
A34: (qz `1 ) ^2 = (|.q.| ^2 ) * ((sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) ^2 ) by A27
.= (|.q.| ^2 ) * (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )) by A33, SQUARE_1:def 4 ;
|.qz.| ^2 = ((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) by JGRAPH_3:10
.= |.q.| ^2 by A27, A34 ;
then sqrt (|.qz.| ^2 ) = |.q.| by SQUARE_1:89;
then A35: |.qz.| = |.q.| by SQUARE_1:89;
|.((0. (TOP-REAL 2)) + (- q)).| < r by A22, EUCLID:45;
then |.(- q).| < r by EUCLID:31;
then |.q.| < r by TOPRNS_1:27;
then |.(- qz).| < r by A35, TOPRNS_1:27;
then |.((0. (TOP-REAL 2)) + (- qz)).| < r by EUCLID:31;
then |.((0. (TOP-REAL 2)) - qz).| < r by EUCLID:45;
then dist u0,pz < r by JGRAPH_1:45;
hence z in W1 by METRIC_1:12; :: thesis: verum

end;

suppose A36: ( q <> 0. (TOP-REAL 2) & (q `2 ) / |.q.| < sn & q `1 <= 0 ) ; :: thesis: z in W1

then A37: (sn -FanMorphW ) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| by A1, Th25;
|.q.| <> 0 by A36, TOPRNS_1:25;
then A38: |.q.| ^2 > 0 by SQUARE_1:74;
A39: sn - ((q `2 ) / |.q.|) >= 0 by A36, XREAL_1:50;
A40: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
A41: 1 + sn > 0 by A1, XREAL_1:150;
A42: ( qz `1 = |.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))) & qz `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)) ) by A21, A37, EUCLID:56;
0 <= (q `1 ) ^2 by XREAL_1:65;
then 0 + ((q `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by XREAL_1:9;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 ) by A40, XREAL_1:74;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= 1 by A38, XCMPLX_1:60;
then ((q `2 ) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (q `2 ) / |.q.| by SQUARE_1:121;
then - (- 1) >= - ((q `2 ) / |.q.|) by XREAL_1:26;
then A43: 1 + sn >= (- ((q `2 ) / |.q.|)) + sn by XREAL_1:9;
(- (1 + sn)) / (1 + sn) <= (- (((q `2 ) / |.q.|) - sn)) / (1 + sn) by A39, A41, XREAL_1:74;
then A44: - 1 <= (- (((q `2 ) / |.q.|) - sn)) / (1 + sn) by A41, XCMPLX_1:198;
(- (((q `2 ) / |.q.|) - sn)) / (1 + sn) <= 1 by A41, A43, XREAL_1:187;
then ((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A44, SQUARE_1:119;
then 1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 ) >= 0 by XREAL_1:50;
then A45: 1 - ((- ((((q `2 ) / |.q.|) - sn) / (1 + sn))) ^2 ) >= 0 by XCMPLX_1:188;
A46: (qz `1 ) ^2 = (|.q.| ^2 ) * ((sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) ^2 ) by A42
.= (|.q.| ^2 ) * (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )) by A45, SQUARE_1:def 4 ;
|.qz.| ^2 = ((qz `1 ) ^2 ) + ((qz `2 ) ^2 ) by JGRAPH_3:10
.= |.q.| ^2 by A42, A46 ;
then sqrt (|.qz.| ^2 ) = |.q.| by SQUARE_1:89;
then A47: |.qz.| = |.q.| by SQUARE_1:89;
|.((0. (TOP-REAL 2)) + (- q)).| < r by A22, EUCLID:45;
then |.(- q).| < r by EUCLID:31;
then |.q.| < r by TOPRNS_1:27;
then |.(- qz).| < r by A47, TOPRNS_1:27;
then |.((0. (TOP-REAL 2)) + (- qz)).| < r by EUCLID:31;
then |.((0. (TOP-REAL 2)) - qz).| < r by EUCLID:45;
then dist u0,pz < r by JGRAPH_1:45;
hence z in W1 by METRIC_1:12; :: thesis: verum

end;

end;

end;

hence ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) by A18, A19, A20, XBOOLE_1:1; :: thesis: verum

end;

then f is continuous by A2, A3, A4, A16, JGRAPH_3:13;
hence ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphW & h is continuous ) ; :: thesis: verum