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:91, 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:72
.= y by A2, A3, A5, A6, Th11
.= (id (Tcircle o,r)) . x by A2, A3, A5, FUNCT_1:35 ; :: thesis: verum

end;

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