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;
hence f .: (U_FT (x,0)) c= U_FT (y,n) by A4; :: thesis: verum

end;

hence f is_continuous n ; :: thesis: verum