theorem :: FINTOPO4:15

for FT1 being non empty RelStr
for FT2 being non empty filled RelStr
for n0, n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n