let r be non negative Real; :: thesis: for n being non zero Element of NAT
for o being Point of (TOP-REAL n)
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 (TOP-REAL n)
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 (TOP-REAL n); :: 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 (TOP-REAL n) such that
A5: y = x and
A6: ( z = f . x & HC (x,f) = HC (z,y,o,r) ) by A1, Def4;
x in halfline (z,y) by A5, TOPREAL9:28;
then x in (halfline (z,y)) /\ (Sphere (o,r)) by A2, A4, XBOOLE_0:def 4;
hence HC (x,f) = x by A3, A5, A6, Def3; :: thesis: verum