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;

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 )
;

end;

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;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

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;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