:: deftheorem Def5 defines BR-map BROUWER:def 5 :
for n being non zero Element of NAT
for r being non negative Real
for o being Point of (TOP-REAL n)
for f being Function of (Tdisk (o,r)),(Tdisk (o,r))
for b₅ being Function of (Tdisk (o,r)),(Tcircle (o,r)) holds
( b₅ = BR-map f iff for x being Point of (Tdisk (o,r)) holds b₅ . x = HC (x,f) );