let n be non empty Element of NAT ; :: thesis: for o, p being Point of (TOP-REAL n)
for r being positive real number st p in Ball o,r holds
(DiskProj o,r,p) | (Sphere o,r) = id (Sphere o,r)
let o, p be Point of (TOP-REAL n); :: thesis: for r being positive real number st p in Ball o,r holds
(DiskProj o,r,p) | (Sphere o,r) = id (Sphere o,r)
let r be positive real number ; :: thesis: ( p in Ball o,r implies (DiskProj o,r,p) | (Sphere o,r) = id (Sphere o,r) )
assume A1: p in Ball o,r ; :: thesis: (DiskProj o,r,p) | (Sphere o,r) = id (Sphere o,r)
A2: the carrier of (Tdisk o,r) = cl_Ball o,r by BROUWER:3;
A3: the carrier of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})) = (cl_Ball o,r) \ {p} by PRE_TOPC:29;
A4: dom (DiskProj o,r,p) = the carrier of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})) by FUNCT_2:def 1;
A5: Sphere o,r misses Ball o,r by TOPREAL9:19;
A6: Sphere o,r c= cl_Ball o,r by TOPREAL9:17;
A7: Ball o,r c= cl_Ball o,r by TOPREAL9:16;
A8: Sphere o,r c= (cl_Ball o,r) \ {p}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Sphere o,r or a in (cl_Ball o,r) \ {p} )
assume A9: a in Sphere o,r ; :: thesis: a in (cl_Ball o,r) \ {p}
then a <> p by A1, A5, XBOOLE_0:3;
hence a in (cl_Ball o,r) \ {p} by A6, A9, ZFMISC_1:64; :: thesis: verum

end;

then A10: dom ((DiskProj o,r,p) | (Sphere o,r)) = Sphere o,r by A3, A4, RELAT_1:91;
A11: dom (id (Sphere o,r)) = Sphere o,r by RELAT_1:71;

now

let x be set ; :: thesis: ( x in dom ((DiskProj o,r,p) | (Sphere o,r)) implies ((DiskProj o,r,p) | (Sphere o,r)) . x = (id (Sphere o,r)) . x )
assume A12: x in dom ((DiskProj o,r,p) | (Sphere o,r)) ; :: thesis: ((DiskProj o,r,p) | (Sphere o,r)) . x = (id (Sphere o,r)) . x
then consider y being Point of (TOP-REAL n) such that
A13: x = y and
A14: (DiskProj o,r,p) . x = HC p,y,o,r by A1, A2, A7, Def7;
y in halfline p,y by TOPREAL9:28;
then A15: x in (halfline p,y) /\ (Sphere o,r) by A10, A12, A13, XBOOLE_0:def 4;
A16: x <> p by A1, A5, A10, A12, XBOOLE_0:3;
thus ((DiskProj o,r,p) | (Sphere o,r)) . x = (DiskProj o,r,p) . x by A12, FUNCT_1:70
.= x by A1, A2, A6, A7, A10, A12, A13, A14, A15, A16, BROUWER:def 3
.= (id (Sphere o,r)) . x by A10, A12, FUNCT_1:35 ; :: thesis: verum

end;

hence (DiskProj o,r,p) | (Sphere o,r) = id (Sphere o,r) by A3, A4, A8, A11, FUNCT_1:9, RELAT_1:91; :: thesis: verum