let sn be Real; ( - 1 < sn & sn < 1 implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = sn -FanMorphE & f is being_homeomorphism ) )
reconsider f = sn -FanMorphE as Function of (TOP-REAL 2),(TOP-REAL 2) ;
assume A1:
( - 1 < sn & sn < 1 )
; ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = sn -FanMorphE & f is being_homeomorphism )
then A2:
for p2 being Point of (TOP-REAL 2) ex K being non empty compact Subset of (TOP-REAL 2) st
( K = f .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & f . p2 in V2 ) )
by Th104;
( rng (sn -FanMorphE) = the carrier of (TOP-REAL 2) & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = sn -FanMorphE & h is continuous ) )
by A1, Th101, Th103;
then
f is being_homeomorphism
by A1, A2, Th3, Th102;
hence
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = sn -FanMorphE & f is being_homeomorphism )
; verum