let r be non negative Real; :: thesis: for o being Point of ()
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint

let o be Point of (); :: 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:
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:
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 ;
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 ;
g is continuous by ;
hence contradiction by A3, A5; :: thesis: verum
end;
suppose not r is positive ; :: thesis:
then reconsider r = r as non positive non negative Real ;
take o ; :: according to ABIAN:def 5 :: thesis:
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 ; :: 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 ; :: thesis: verum
end;
end;