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 that
A1: f is_continuous n0 and
A2: 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 that
x in the carrier of FT1 and
A3: y = f . x ; :: thesis: f .: (U_FT x,0 ) c= U_FT y,n
( U_FT y,n0 = Finf (U_FT y),n0 & 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 A2, Th1;
f .: (U_FT x,0 ) c= U_FT y,n0 by A1, A3, 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