let r be non negative real number ; :: thesis: for n being non empty 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 empty 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, ABIAN:def 4;
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