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 ; :: thesis: verum