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

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