defpred S1[ Point of (Tdisk (o,r)), set ] means $2 = HC ($1,f);
A1:
for x being Point of (Tdisk (o,r)) ex m being Point of (Tcircle (o,r)) st S1[x,m]
;
ex h being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds S1[x,h . x]
from FUNCT_2:sch 3(A1);
hence
ex b1 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f)
; verum