reconsider D = NonZero (TOP-REAL 2) as non empty Subset of (TOP-REAL 2) by JGRAPH_2:9;
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 that
A1: - 1 < sn and
A2: 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) ;
A3: f . (0. (TOP-REAL 2)) = 0. (TOP-REAL 2) by Th16, JGRAPH_2:3;
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 5;
then reconsider q = p as Point of (TOP-REAL 2) by XBOOLE_0:def 5;
not p in {(0. (TOP-REAL 2))} by A5, XBOOLE_0:def 5;
then A6: p <> 0. (TOP-REAL 2) by 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 A7: ( (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)))]|;
A8: |[(|.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:52;
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)))) by EUCLID:52;
now :: thesis: not |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| = 0. (TOP-REAL 2)
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 A6, TOPRNS_1:24;
then - (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))) = - (sqrt (1 - 0)) by A8, A10, JGRAPH_2:3, XCMPLX_1:6
.= - 1 by SQUARE_1:18 ;
hence contradiction by A9, A10, A11, JGRAPH_2:3, XCMPLX_1:6; :: thesis: verum
end;
hence f . p <> f . (0. (TOP-REAL 2)) by A1, A2, A3, A6, A7, Th18; :: 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)))]| `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)) by EUCLID:52;
A14: |[(|.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)))) by EUCLID:52;
now :: thesis: not |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| = 0. (TOP-REAL 2)
assume A15: |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
A16: |.q.| <> 0 ^2 by A6, TOPRNS_1:24;
then - (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))) = - (sqrt (1 - 0)) by A13, A15, JGRAPH_2:3, XCMPLX_1:6
.= - 1 by SQUARE_1:18 ;
hence contradiction by A14, A15, A16, JGRAPH_2:3, XCMPLX_1:6; :: thesis: verum
end;
hence f . p <> f . (0. (TOP-REAL 2)) by A1, A2, A3, A6, A12, Th18; :: thesis: verum
end;
suppose q `1 > 0 ; :: thesis: f . p <> f . (0. (TOP-REAL 2))
then f . p = p by Th16;
hence f . p <> f . (0. (TOP-REAL 2)) by A6, Th16, JGRAPH_2:3; :: thesis: verum
end;
end;
end;
A17: 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
reconsider u0 = 0. (TOP-REAL 2) as Point of (Euclid 2) by EUCLID:67;
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 ) )
reconsider VV = V as Subset of (TopSpaceMetr (Euclid 2)) by Lm11;
assume that
A18: f . (0. (TOP-REAL 2)) in V and
A19: 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 )
VV is open by A19, Lm11, PRE_TOPC:30;
then consider r being Real such that
A20: r > 0 and
A21: Ball (u0,r) c= V by A3, A18, TOPMETR:15;
reconsider r = r as Real ;
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) ;
A22: W1 is open by GOBOARD6:3;
A23: f .: W1 c= W1
proof
let z be object ; :: 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 object such that
A24: y in dom f and
A25: y in W1 and
A26: z = f . y by FUNCT_1:def 6;
z in rng f by A24, A26, FUNCT_1:def 3;
then reconsider qz = z as Point of (TOP-REAL 2) ;
reconsider pz = qz as Point of (Euclid 2) by EUCLID:67;
reconsider q = y as Point of (TOP-REAL 2) by A24;
reconsider qy = q as Point of (Euclid 2) by EUCLID:67;
dist (u0,qy) < r by A25, METRIC_1:11;
then A27: |.((0. (TOP-REAL 2)) - q).| < r by JGRAPH_1:28;
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:3;
suppose A28: ( q <> 0. (TOP-REAL 2) & (q `2) / |.q.| >= sn & q `1 <= 0 ) ; :: thesis: z in W1
then A29: ((q `2) / |.q.|) - sn >= 0 by XREAL_1:48;
0 <= (q `1) ^2 by XREAL_1:63;
then ( |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) & 0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then A30: ((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2) by XREAL_1:72;
A31: 1 - sn > 0 by A2, XREAL_1:149;
|.q.| <> 0 by A28, TOPRNS_1:24;
then |.q.| ^2 > 0 by SQUARE_1:12;
then ((q `2) ^2) / (|.q.| ^2) <= 1 by A30, XCMPLX_1:60;
then ((q `2) / |.q.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (q `2) / |.q.| by SQUARE_1:51;
then 1 - sn >= ((q `2) / |.q.|) - sn by XREAL_1:9;
then - (1 - sn) <= - (((q `2) / |.q.|) - sn) by XREAL_1:24;
then (- (1 - sn)) / (1 - sn) <= (- (((q `2) / |.q.|) - sn)) / (1 - sn) by A31, XREAL_1:72;
then - 1 <= (- (((q `2) / |.q.|) - sn)) / (1 - sn) by A31, XCMPLX_1:197;
then ((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A31, A29, SQUARE_1:49;
then 1 - (((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2) >= 0 by XREAL_1:48;
then A32: 1 - ((- ((((q `2) / |.q.|) - sn) / (1 - sn))) ^2) >= 0 by XCMPLX_1:187;
A33: (sn -FanMorphW) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| by A1, A2, A28, Th18;
then A34: qz `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)) by A26, EUCLID:52;
qz `1 = |.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))) by A26, A33, EUCLID:52;
then A35: (qz `1) ^2 = (|.q.| ^2) * ((sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))) ^2)
.= (|.q.| ^2) * (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)) by A32, SQUARE_1:def 2 ;
|.qz.| ^2 = ((qz `1) ^2) + ((qz `2) ^2) by JGRAPH_3:1
.= |.q.| ^2 by A34, A35 ;
then sqrt (|.qz.| ^2) = |.q.| by SQUARE_1:22;
then A36: |.qz.| = |.q.| by SQUARE_1:22;
|.(- q).| < r by A27, RLVECT_1:4;
then |.q.| < r by TOPRNS_1:26;
then |.(- qz).| < r by A36, TOPRNS_1:26;
then |.((0. (TOP-REAL 2)) - qz).| < r by RLVECT_1:4;
then dist (u0,pz) < r by JGRAPH_1:28;
hence z in W1 by METRIC_1:11; :: thesis: verum
end;
suppose A37: ( q <> 0. (TOP-REAL 2) & (q `2) / |.q.| < sn & q `1 <= 0 ) ; :: thesis: z in W1
0 <= (q `1) ^2 by XREAL_1:63;
then ( |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) & 0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then A38: ((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2) by XREAL_1:72;
A39: 1 + sn > 0 by A1, XREAL_1:148;
|.q.| <> 0 by A37, TOPRNS_1:24;
then |.q.| ^2 > 0 by SQUARE_1:12;
then ((q `2) ^2) / (|.q.| ^2) <= 1 by A38, XCMPLX_1:60;
then ((q `2) / |.q.|) ^2 <= 1 by XCMPLX_1:76;
then - 1 <= (q `2) / |.q.| by SQUARE_1:51;
then - (- 1) >= - ((q `2) / |.q.|) by XREAL_1:24;
then 1 + sn >= (- ((q `2) / |.q.|)) + sn by XREAL_1:7;
then A40: (- (((q `2) / |.q.|) - sn)) / (1 + sn) <= 1 by A39, XREAL_1:185;
sn - ((q `2) / |.q.|) >= 0 by A37, XREAL_1:48;
then - 1 <= (- (((q `2) / |.q.|) - sn)) / (1 + sn) by A39;
then ((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2 <= 1 ^2 by A40, SQUARE_1:49;
then 1 - (((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2) >= 0 by XREAL_1:48;
then A41: 1 - ((- ((((q `2) / |.q.|) - sn) / (1 + sn))) ^2) >= 0 by XCMPLX_1:187;
A42: (sn -FanMorphW) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| by A1, A2, A37, Th18;
then A43: qz `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)) by A26, EUCLID:52;
qz `1 = |.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))) by A26, A42, EUCLID:52;
then A44: (qz `1) ^2 = (|.q.| ^2) * ((sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))) ^2)
.= (|.q.| ^2) * (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)) by A41, SQUARE_1:def 2 ;
|.qz.| ^2 = ((qz `1) ^2) + ((qz `2) ^2) by JGRAPH_3:1
.= |.q.| ^2 by A43, A44 ;
then sqrt (|.qz.| ^2) = |.q.| by SQUARE_1:22;
then A45: |.qz.| = |.q.| by SQUARE_1:22;
|.(- q).| < r by A27, RLVECT_1:4;
then |.q.| < r by TOPRNS_1:26;
then |.(- qz).| < r by A45, TOPRNS_1:26;
then |.((0. (TOP-REAL 2)) - qz).| < r by RLVECT_1:4;
then dist (u0,pz) < r by JGRAPH_1:28;
hence z in W1 by METRIC_1:11; :: thesis: verum
end;
end;
end;
u0 in W1 by A20, GOBOARD6:1;
hence ex W being Subset of (TOP-REAL 2) st
( 0. (TOP-REAL 2) in W & W is open & f .: W c= V ) by A21, A22, A23, XBOOLE_1:1; :: thesis: verum
end;
A46: D ` = {(0. (TOP-REAL 2))} by JGRAPH_3:20;
then ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphW) | D & h is continuous ) by A1, A2, Th36;
hence ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphW & h is continuous ) by A3, A46, A4, A17, JGRAPH_3:3; :: thesis: verum