let FT1 be non empty RelStr ; :: thesis: 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
let FT2 be non empty filled RelStr ; :: thesis: 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
let n0, n be Element of NAT ; :: thesis: for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n
let f be Function of FT1,FT2; :: thesis: ( f is_continuous n0 & n0 <= n implies f is_continuous n )
assume A1: ( f is_continuous n0 & n0 <= n ) ; :: 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 A2: ( x in the carrier of FT1 & y = f . x ) ; :: thesis: f .: (U_FT x,0 ) c= U_FT y,n
A3: U_FT y,n0 = Finf (U_FT y),n0 by FINTOPO3:def 10;
U_FT y,n = Finf (U_FT y),n by FINTOPO3:def 10;
then A4: U_FT y,n0 c= U_FT y,n by A1, A3, Th1;
f .: (U_FT x,0 ) c= U_FT y,n0 by A1, A2, Def2;
hence f .: (U_FT x,0 ) c= U_FT y,n by A4, XBOOLE_1:1; :: thesis: verum

end;

hence f is_continuous n by Def2; :: thesis: verum