let cn be Real; :: thesis: ( - 1 < cn & cn < 1 implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = cn -FanMorphN & f is being_homeomorphism ) )
reconsider f = cn -FanMorphN as Function of (TOP-REAL 2),(TOP-REAL 2) ;
assume A1: ( - 1 < cn & cn < 1 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = cn -FanMorphN & 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 Th73;
( rng (cn -FanMorphN) = the carrier of (TOP-REAL 2) & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h = cn -FanMorphN & h is continuous ) ) by A1, Th70, Th72;
then f is being_homeomorphism by A1, A2, Th3, Th71;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = cn -FanMorphN & f is being_homeomorphism ) ; :: thesis: verum