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