let r be non negative Real; :: thesis: for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x
let o be Point of (TOP-REAL 2); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: ex x being Point of (Tdisk (o,r)) st f . x = x
f is with_fixpoint by Th14;
then consider x being object such that
A1: x is_a_fixpoint_of f ;
reconsider x = x as set by TARSKI:1;
take x ; :: thesis: ( x is Point of (Tdisk (o,r)) & f . x = x )
x in dom f by A1;
hence x is Point of (Tdisk (o,r)) ; :: thesis: f . x = x
thus f . x = x by A1; :: thesis: verum