let sn be Real; :: thesis: for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphW ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let K0, B0 be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphW ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); :: thesis: ( - 1 < sn & sn < 1 & f = (sn -FanMorphW ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
assume A1: ( - 1 < sn & sn < 1 & f = (sn -FanMorphW ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous
set cn = sqrt (1 - (sn ^2 ));
set p0 = |[(sqrt (1 - (sn ^2 ))),(- sn)]|;
A2: |[(sqrt (1 - (sn ^2 ))),(- sn)]| `1 = sqrt (1 - (sn ^2 )) by EUCLID:56;
sn ^2 < 1 ^2 by A1, SQUARE_1:120;
then A3: 1 - (sn ^2 ) > 0 by XREAL_1:52;
then A4: |[(sqrt (1 - (sn ^2 ))),(- sn)]| <> 0. (TOP-REAL 2) by A2, JGRAPH_2:11, SQUARE_1:93;
|[(sqrt (1 - (sn ^2 ))),(- sn)]| `1 > 0 by A2, A3, SQUARE_1:93;
then |[(sqrt (1 - (sn ^2 ))),(- sn)]| in K0 by A1, JGRAPH_2:11;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
( |[(sqrt (1 - (sn ^2 ))),(- sn)]| in the carrier of (TOP-REAL 2) & not |[(sqrt (1 - (sn ^2 ))),(- sn)]| in {(0. (TOP-REAL 2))} ) by A4, TARSKI:def 1;
then reconsider D = B0 as non empty Subset of (TOP-REAL 2) by A1, XBOOLE_0:def 5;
A5: K1 c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 or x in D )
assume x in K1 ; :: thesis: x in D
then consider p2 being Point of (TOP-REAL 2) such that
A6: ( p2 = x & p2 `1 >= 0 & p2 <> 0. (TOP-REAL 2) ) by A1;
not p2 in {(0. (TOP-REAL 2))} by A6, TARSKI:def 1;
hence x in D by A1, A6, XBOOLE_0:def 5; :: thesis: verum

end;

for p being Point of ((TOP-REAL 2) | K1)
for V being Subset of ((TOP-REAL 2) | D) st f . p in V & V is open holds
ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )

proof

let p be Point of ((TOP-REAL 2) | K1); :: thesis: for V being Subset of ((TOP-REAL 2) | D) st f . p in V & V is open holds
ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )
let V be Subset of ((TOP-REAL 2) | D); :: thesis: ( f . p in V & V is open implies ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V ) )
assume A7: ( f . p in V & V is open ) ; :: thesis: ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )
then consider V2 being Subset of (TOP-REAL 2) such that
A8: ( V2 is open & V2 /\ ([#] ((TOP-REAL 2) | D)) = V ) by TOPS_2:32;
A9: p in the carrier of ((TOP-REAL 2) | K1) ;
A10: [#] ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:def 10;
reconsider W2 = V2 /\ ([#] ((TOP-REAL 2) | K1)) as Subset of ((TOP-REAL 2) | K1) ;
A11: W2 is open by A8, TOPS_2:32;
A12: f . p = (sn -FanMorphW ) . p by A1, A10, FUNCT_1:72;
consider q being Point of (TOP-REAL 2) such that
A13: ( q = p & q `1 >= 0 & q <> 0. (TOP-REAL 2) ) by A1, A9, A10;
(sn -FanMorphW ) . q = q by A13, Th23;
then ( p in V2 & p in [#] ((TOP-REAL 2) | D) ) by A7, A8, A12, A13, XBOOLE_0:def 4;
then A14: p in W2 by XBOOLE_0:def 4;
f .: W2 c= V

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: W2 or y in V )
assume y in f .: W2 ; :: thesis: y in V
then consider x being set such that
A15: ( x in dom f & x in W2 & y = f . x ) by FUNCT_1:def 12;
f is Function of ((TOP-REAL 2) | K1),((TOP-REAL 2) | D) ;
then dom f = K1 by A10, FUNCT_2:def 1;
then consider p4 being Point of (TOP-REAL 2) such that
A16: ( x = p4 & p4 `1 >= 0 & p4 <> 0. (TOP-REAL 2) ) by A1, A15;
A17: f . p4 = (sn -FanMorphW ) . p4 by A1, A10, A15, A16, FUNCT_1:72
.= p4 by A16, Th23 ;
A18: ( p4 in V2 & p4 in [#] ((TOP-REAL 2) | K1) ) by A15, A16, XBOOLE_0:def 4;
then p4 in D by A5, A10;
then p4 in [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 10;
hence y in V by A8, A15, A16, A17, A18, XBOOLE_0:def 4; :: thesis: verum

end;

hence ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V ) by A11, A14; :: thesis: verum

end;

hence f is continuous by JGRAPH_2:20; :: thesis: verum