let r be non negative real number ; :: thesis: for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f has_no_fixpoint holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let n be non empty Element of NAT ; :: thesis: for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f has_no_fixpoint holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let o be Point of (TOP-REAL n); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f has_no_fixpoint holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: ( f has_no_fixpoint implies (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) )
assume A1: f has_no_fixpoint ; :: thesis: (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
set D = cl_Ball (o,r);
set C = Sphere (o,r);
set g = BR-map f;
( dom (BR-map f) = the carrier of (Tdisk (o,r)) & the carrier of (Tdisk (o,r)) = cl_Ball (o,r) ) by Th3, FUNCT_2:def 1;
then A2: dom ((BR-map f) | (Sphere (o,r))) = Sphere (o,r) by RELAT_1:62, TOPREAL9:17;
A3: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
A4: for x being set st x in dom ((BR-map f) | (Sphere (o,r))) holds
((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x

proof

let x be set ; :: thesis: ( x in dom ((BR-map f) | (Sphere (o,r))) implies ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x )
assume A5: x in dom ((BR-map f) | (Sphere (o,r))) ; :: thesis: ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x
reconsider y = x as Point of (Tdisk (o,r)) by A5;
A6: not x is_a_fixpoint_of f by A1, ABIAN:def 5;
thus ((BR-map f) | (Sphere (o,r))) . x = (BR-map f) . x by A2, A5, FUNCT_1:49
.= y by A2, A3, A5, A6, Th11
.= (id (Tcircle (o,r))) . x by A2, A3, A5, FUNCT_1:18 ; :: thesis: verum

end;

dom (id (Tcircle (o,r))) = the carrier of (Tcircle (o,r)) by RELAT_1:45;
hence (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) by A2, A3, A4, FUNCT_1:2; :: thesis: verum