let r be non negative real number ; :: 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 has_a_fixpoint by Th14;
then consider x being set such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
take x ; :: thesis: ( x is Point of (Tdisk o,r) & f . x = x )
x in dom f by A1, ABIAN:def 3;
hence x is Point of (Tdisk o,r) ; :: thesis: f . x = x
thus f . x = x by A1, ABIAN:def 3; :: thesis: verum