let FT1 be non empty RelStr ; :: thesis: for FT2 being non empty filled RelStr
for n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
let FT2 be non empty filled RelStr ; :: thesis: for n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
let n be Element of NAT ; :: thesis: for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
let f be Function of FT1,FT2; :: thesis: ( f is_continuous 0 implies f is_continuous n )
assume A1: f is_continuous 0 ; :: thesis: f is_continuous n
for x being Element of FT1
for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n)

proof

let x be Element of FT1; :: thesis: for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n)
let y be Element of FT2; :: thesis: ( x in the carrier of FT1 & y = f . x implies f .: (U_FT (x,0)) c= U_FT (y,n) )
assume that
x in the carrier of FT1 and
A2: y = f . x ; :: thesis: f .: (U_FT (x,0)) c= U_FT (y,n)
( U_FT y = U_FT (y,0) & U_FT (y,n) = Finf ((U_FT y),n) ) by FINTOPO3:47, FINTOPO3:def 10;
then A3: U_FT (y,0) c= U_FT (y,n) by FINTOPO3:36;
f .: (U_FT (x,0)) c= U_FT (y,0) by A1, A2;
hence f .: (U_FT (x,0)) c= U_FT (y,n) by A3; :: thesis: verum

end;

hence f is_continuous n ; :: thesis: verum