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

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

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

dom (id (Tcircle (o,r))) = the carrier of (Tcircle (o,r))
;
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;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

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