let X be discrete TopSpace; :: thesis: for Y being TopSpace
for f being Function of X,Y holds f is continuous
let Y be TopSpace; :: thesis: for f being Function of X,Y holds f is continuous
let f be Function of X,Y; :: thesis: f is continuous
for B being Subset of Y st B is closed holds
f " B is closed by TDLAT_3:18;
hence f is continuous by PRE_TOPC:def 12; :: thesis: verum