for r being non negative Real
for n being non zero Element of NAT
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))