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:16;
hence f is continuous by PRE_TOPC:def 6; :: thesis: verum