theorem Th9: :: BROUWER3:9

for n being Nat
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st p in Fr A & A is closed holds
for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f ) ) )