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)) holds f is with_fixpoint
let o be Point of (TOP-REAL 2); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: f is with_fixpoint
A1: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
A2: the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
per cases ( r is positive or not r is positive ) ;
suppose r is positive ; :: thesis: f is with_fixpoint
then reconsider r = r as positive Real ;
Sphere (o,r) c= cl_Ball (o,r) by TOPREAL9:17;
then reconsider Y = Tcircle (o,r) as non empty SubSpace of Tdisk (o,r) by A1, A2, TSEP_1:4;
reconsider g = BR-map f as Function of (Tdisk (o,r)),Y ;
A3: not Y is_a_retract_of Tdisk (o,r) by Th10;
assume A4: f is without_fixpoints ; :: thesis: contradiction
A5: g is being_a_retraction by A4, Th11;
g is continuous by A4, Th13;
hence contradiction by A3, A5; :: thesis: verum
end;
suppose not r is positive ; :: thesis: f is with_fixpoint
then reconsider r = r as non positive non negative Real ;
take o ; :: according to ABIAN:def 5 :: thesis: o is_a_fixpoint_of f
A6: cl_Ball (o,r) = {o} by Th2;
dom f = the carrier of (Tdisk (o,r)) by FUNCT_2:def 1;
hence o in dom f by A2, A6, TARSKI:def 1; :: according to ABIAN:def 3 :: thesis: o = f . o
then f . o in rng f by FUNCT_1:def 3;
hence o = f . o by A2, A6, TARSKI:def 1; :: thesis: verum
end;
end;