let r be non negative Real; :: thesis: for n being non zero 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 is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let n be non zero 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 is without_fixpoints 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 is without_fixpoints 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 is without_fixpoints implies (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) )
assume A1: f is without_fixpoints ; :: 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 object 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 object ; :: 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
x in dom (BR-map f) by A5, RELAT_1:57;
then reconsider y = x as Point of (Tdisk (o,r)) ;
A6: not x is_a_fixpoint_of f by A1;
thus ((BR-map f) | (Sphere (o,r))) . x = (BR-map f) . x by A5, FUNCT_1:49
.= y by A3, A5, A6, Th11
.= (id (Tcircle (o,r))) . x by A3, A5, FUNCT_1:18 ; :: thesis: verum

end;

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