let cn be Real; :: thesis: ( - 1 < cn & cn < 1 implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = cn -FanMorphS & f is being_homeomorphism ) )
assume A1: ( - 1 < cn & cn < 1 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = cn -FanMorphS & f is being_homeomorphism )
then A2: ( cn -FanMorphS is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (cn -FanMorphS ) = the carrier of (TOP-REAL 2) ) by Th141;
set f = cn -FanMorphS ;
A3: cn -FanMorphS is continuous by A1, Th139;
A4: cn -FanMorphS is one-to-one by A1, Th140;
for p2 being Point of (TOP-REAL 2) ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (cn -FanMorphS ) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (cn -FanMorphS ) . p2 in V2 ) ) by A1, Th142;
then cn -FanMorphS is being_homeomorphism by A2, A3, A4, Th8;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f = cn -FanMorphS & f is being_homeomorphism ) ; :: thesis: verum