let r be non negative real number ; :: thesis: for n being non empty Element of NAT
for o being Point of
for x being Point of
for f being Function of (Tdisk o,r),(Tdisk o,r) st not x is_a_fixpoint_of f & x is Point of holds
(BR-map f) . x = x
let n be non empty Element of NAT ; :: thesis: for o being Point of
for x being Point of
for f being Function of (Tdisk o,r),(Tdisk o,r) st not x is_a_fixpoint_of f & x is Point of holds
(BR-map f) . x = x
let o be Point of ; :: thesis: for x being Point of
for f being Function of (Tdisk o,r),(Tdisk o,r) st not x is_a_fixpoint_of f & x is Point of holds
(BR-map f) . x = x
let x be Point of ; :: thesis: for f being Function of (Tdisk o,r),(Tdisk o,r) st not x is_a_fixpoint_of f & x is Point of 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 implies (BR-map f) . x = x )
assume A1: ( not x is_a_fixpoint_of f & x is Point of ) ; :: thesis: (BR-map f) . x = x
thus (BR-map f) . x = HC x,f by Def5
.= x by A1, Th9 ; :: thesis: verum