let cn 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 < cn & cn < 1 & f = (cn -FanMorphS) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 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 < cn & cn < 1 & f = (cn -FanMorphS) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 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 < cn & cn < 1 & f = (cn -FanMorphS) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
set sn = sqrt (1 - (cn ^2));
set p0 = |[cn,(sqrt (1 - (cn ^2)))]|;
A1: |[cn,(sqrt (1 - (cn ^2)))]| `2 = sqrt (1 - (cn ^2)) by EUCLID:52;
assume A2: ( - 1 < cn & cn < 1 & f = (cn -FanMorphS) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: f is continuous
then cn ^2 < 1 ^2 by SQUARE_1:50;
then A3: 1 - (cn ^2) > 0 by XREAL_1:50;
then sqrt (1 - (cn ^2)) > 0 by SQUARE_1:25;
then |[cn,(sqrt (1 - (cn ^2)))]| in K0 by A2, A1, JGRAPH_2:3;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
|[cn,(sqrt (1 - (cn ^2)))]| `2 > 0 by A1, A3, SQUARE_1:25;
then not |[cn,(sqrt (1 - (cn ^2)))]| in {(0. (TOP-REAL 2))} by JGRAPH_2:3, TARSKI:def 1;
then reconsider D = B0 as non empty Subset of (TOP-REAL 2) by A2, XBOOLE_0:def 5;
A4: K1 c= D

proof

let x be object ; :: 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
A5: p2 = x and
p2 `2 >= 0 and
A6: p2 <> 0. (TOP-REAL 2) by A2;
not p2 in {(0. (TOP-REAL 2))} by A6, TARSKI:def 1;
hence x in D by A2, A5, 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 that
A7: f . p in V and
A8: V is open ; :: thesis: ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V )
consider V2 being Subset of (TOP-REAL 2) such that
A9: V2 is open and
A10: V2 /\ ([#] ((TOP-REAL 2) | D)) = V by A8, TOPS_2:24;
reconsider W2 = V2 /\ ([#] ((TOP-REAL 2) | K1)) as Subset of ((TOP-REAL 2) | K1) ;
A11: [#] ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:def 5;
then A12: f . p = (cn -FanMorphS) . p by A2, FUNCT_1:49;
A13: f .: W2 c= V

proof

let y be object ; :: 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 object such that
A14: x in dom f and
A15: x in W2 and
A16: y = f . x by FUNCT_1:def 6;
f is Function of ((TOP-REAL 2) | K1),((TOP-REAL 2) | D) ;
then dom f = K1 by A11, FUNCT_2:def 1;
then consider p4 being Point of (TOP-REAL 2) such that
A17: x = p4 and
A18: p4 `2 >= 0 and
p4 <> 0. (TOP-REAL 2) by A2, A14;
A19: p4 in V2 by A15, A17, XBOOLE_0:def 4;
p4 in [#] ((TOP-REAL 2) | K1) by A14, A17;
then p4 in D by A4, A11;
then A20: p4 in [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 5;
f . p4 = (cn -FanMorphS) . p4 by A2, A11, A14, A17, FUNCT_1:49
.= p4 by A18, Th113 ;
hence y in V by A10, A16, A17, A19, A20, XBOOLE_0:def 4; :: thesis: verum

end;

p in the carrier of ((TOP-REAL 2) | K1) ;
then consider q being Point of (TOP-REAL 2) such that
A21: q = p and
A22: q `2 >= 0 and
q <> 0. (TOP-REAL 2) by A2, A11;
(cn -FanMorphS) . q = q by A22, Th113;
then p in V2 by A7, A10, A12, A21, XBOOLE_0:def 4;
then A23: p in W2 by XBOOLE_0:def 4;
W2 is open by A9, TOPS_2:24;
hence ex W being Subset of ((TOP-REAL 2) | K1) st
( p in W & W is open & f .: W c= V ) by A23, A13; :: thesis: verum

end;

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