let X be non empty TopSpace; :: thesis: for Y being non empty anti-discrete TopSpace
for f being Function of X,Y holds f is continuous
let Y be non empty anti-discrete TopSpace; :: thesis: for f being Function of X,Y holds f is continuous
let f be Function of X,Y; :: thesis: f is continuous

now :: thesis: for B being Subset of Y st B is closed holds
f " B is closed

let B be Subset of Y; :: thesis: ( B is closed implies f " B is closed )
assume A1: B is closed ; :: thesis: f " B is closed

now :: thesis: f " B is closed

per cases ( B = {} or B = the carrier of Y ) by A1, TDLAT_3:19;

suppose B = {} ; :: thesis: f " B is closed

then f " B = {} X ;
hence f " B is closed ; :: thesis: verum

end;

suppose B = the carrier of Y ; :: thesis: f " B is closed

then B = [#] Y ;
then f " B = [#] X by TOPS_2:41;
hence f " B is closed ; :: thesis: verum

end;

end;

end;

hence f " B is closed ; :: thesis: verum

end;

hence f is continuous by PRE_TOPC:def 6; :: thesis: verum