let r be non negative Real; :: thesis: for n being non zero Element of NAT
for o being Point of ()
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
() | (Sphere (o,r)) = id (Tcircle (o,r))

let n be non zero Element of NAT ; :: thesis: for o being Point of ()
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
() | (Sphere (o,r)) = id (Tcircle (o,r))

let o be Point of (); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
() | (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 () | (Sphere (o,r)) = id (Tcircle (o,r)) )
assume A1: f is without_fixpoints ; :: thesis: () | (Sphere (o,r)) = id (Tcircle (o,r))
set D = cl_Ball (o,r);
set C = Sphere (o,r);
set g = BR-map f;
( dom () = the carrier of (Tdisk (o,r)) & the carrier of (Tdisk (o,r)) = cl_Ball (o,r) ) by ;
then A2: dom (() | (Sphere (o,r))) = Sphere (o,r) by ;
A3: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
A4: for x being object st x in dom (() | (Sphere (o,r))) holds
(() | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x
proof
let x be object ; :: thesis: ( x in dom (() | (Sphere (o,r))) implies (() | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x )
assume A5: x in dom (() | (Sphere (o,r))) ; :: thesis: (() | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x
x in dom () by ;
then reconsider y = x as Point of (Tdisk (o,r)) ;
A6: not x is_a_fixpoint_of f by A1;
thus (() | (Sphere (o,r))) . x = () . x by
.= y by A3, A5, A6, Th11
.= (id (Tcircle (o,r))) . x by ; :: 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 ; :: thesis: verum