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)) holds f has_a_fixpoint
let o be Point of (TOP-REAL 2); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f has_a_fixpoint
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: f has_a_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 has_a_fixpoint

then reconsider r = r as positive real number ;
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 has_no_fixpoint ; :: thesis: contradiction
A5: g is being_a_retraction

proof

let W be Point of (Tdisk (o,r)); :: according to BORSUK_1:def 19 :: thesis: ( not W in the carrier of Y or g . W = W )
assume A6: W in the carrier of Y ; :: thesis: g . W = W
not W is_a_fixpoint_of f by A4, ABIAN:def 5;
hence g . W = W by A6, Th11; :: thesis: verum

end;

g is continuous by A4, Th13;
hence contradiction by A3, A5, BORSUK_1:def 20; :: thesis: verum

end;

suppose not r is positive ; :: thesis: f has_a_fixpoint

then reconsider r = r as non positive non negative real number ;
take o ; :: according to ABIAN:def 5 :: thesis: o is_a_fixpoint_of f
A7: 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, A7, TARSKI:def 1; :: according to ABIAN:def 3 :: thesis: o = f . o
then f . o in rng f by FUNCT_1:def 5;
hence o = f . o by A2, A7, TARSKI:def 1; :: thesis: verum

end;

end;