for n being Nat
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st n > 0 & p in A & ( 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 ) ) ) ) holds
p in Fr A