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

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