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

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