A1: n in NAT by ORDINAL1:def 12;
for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
(CircleIso (p,r)) . a = (r * b) + p by Def5;
hence CircleIso (p,r) is being_homeomorphism by A1, TOPREALB:19; :: thesis: verum