let X be TopSpace; :: thesis: for Y being TopStruct
for f being Function of X,Y st f is empty holds
f is continuous
let Y be TopStruct ; :: thesis: for f being Function of X,Y st f is empty holds
f is continuous
let f be Function of X,Y; :: thesis: ( f is empty implies f is continuous )
assume A1: f is empty ; :: thesis: f is continuous
let P be Subset of Y; :: according to PRE_TOPC:def 6 :: thesis: ( not P is closed or f " P is closed )
assume P is closed ; :: thesis: f " P is closed
f " P = {} X by A1;
hence f " P is closed ; :: thesis: verum