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
() . x = 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
() . x = 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
() . x = 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
() . x = 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 () . x = x )
assume A1: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) ) ; :: thesis: () . x = x
thus () . x = HC (x,f) by Def5
.= x by ; :: thesis: verum