for n being Nat
for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds
for F being closed Subset of TM st ind (F `) <= n holds
for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f