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
(BR-map f) . x = 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
(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 that
A1: not x is_a_fixpoint_of f and
A2: 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, A2, Th9 ; :: thesis: verum