let r be non negative Real; 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 ; 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); 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)); 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)); ( 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)) )
; (BR-map f) . x = x
thus (BR-map f) . x =
HC (x,f)
by Def5
.=
x
by A1, Th9
; verum