let r be non negative Real; :: thesis: for n being non zero Element of NAT
for o being Point of ()
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x

let n be non zero Element of NAT ; :: thesis: for o being Point of ()
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x

let o be Point of (); :: thesis: for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x

let x be Point of (Tdisk (o,r)); :: thesis: for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x

let f be Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) implies HC (x,f) = x )
assume that
A1: not x is_a_fixpoint_of f and
A2: x is Point of (Tcircle (o,r)) ; :: thesis: HC (x,f) = x
A3: x <> f . x by A1;
A4: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
consider y, z being Point of () such that
A5: y = x and
A6: ( z = f . x & HC (x,f) = HC (z,y,o,r) ) by ;
x in halfline (z,y) by ;
then x in (halfline (z,y)) /\ (Sphere (o,r)) by ;
hence HC (x,f) = x by A3, A5, A6, Def3; :: thesis: verum