theorem :: FINTOPO5:10

for kc, km being Nat
for n being non zero Nat
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)