for n being Nat
for r being non negative Real
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n) holds f (-) is Function of (Tcircle ((0. (TOP-REAL (n + 1))),r)),(TOP-REAL n)