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 A3: r is positive ; :: thesis: f has_a_fixpoint

assume A4: f has_no_fixpoint ; :: thesis: contradiction
reconsider r = r as positive real number by A3;
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;
A5: not Y is_a_retract_of Tdisk o,r by Th10;
reconsider g = BR-map f as Function of (Tdisk o,r),Y ;
A6: g is continuous by A4, Th13;
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 A7: 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 A7, Th11; :: thesis: verum

end;

hence contradiction by A5, A6, 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 ;
A8: cl_Ball o,r = {o} by Th2;
take o ; :: according to ABIAN:def 5 :: thesis: o is_a_fixpoint_of f
dom f = the carrier of (Tdisk o,r) by FUNCT_2:def 1;
hence o in dom f by A2, A8, 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, A8, TARSKI:def 1; :: thesis: verum

end;

end;