let cn be Real; :: thesis: for B0 being Subset of (TOP-REAL 2)
for K0 being Subset of ((TOP-REAL 2) | B0)
for f being Function of (((TOP-REAL 2) | B0) | 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 B0 be Subset of (TOP-REAL 2); :: thesis: for K0 being Subset of ((TOP-REAL 2) | B0)
for f being Function of (((TOP-REAL 2) | B0) | 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 be Subset of ((TOP-REAL 2) | B0); :: thesis: for f being Function of (((TOP-REAL 2) | B0) | 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) | B0) | 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 )
the carrier of ((TOP-REAL 2) | B0) = B0 by PRE_TOPC:8;
then reconsider K1 = K0 as Subset of (TOP-REAL 2) by XBOOLE_1:1;
assume A1: ( - 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
K0 c= B0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K0 or x in B0 )
assume x in K0 ; :: thesis: x in B0
then A2: ex p8 being Point of (TOP-REAL 2) st
( x = p8 & p8 `2 >= 0 & p8 <> 0. (TOP-REAL 2) ) by A1;
then not x in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence x in B0 by A1, A2, XBOOLE_0:def 5; :: thesis: verum

end;

then ((TOP-REAL 2) | B0) | K0 = (TOP-REAL 2) | K1 by PRE_TOPC:7;
hence f is continuous by A1, Th125; :: thesis: verum