for n being non zero Element of NAT
for r being positive Real
for x being Point of (TOP-REAL n)
for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism