let NTX, NTY be NTopSpace; :: thesis: for A being Subset of NTX
for f being continuous Function of NTX,NTY holds f .: (Cl A) c= Cl (f .: A)
let A be Subset of NTX; :: thesis: for f being continuous Function of NTX,NTY holds f .: (Cl A) c= Cl (f .: A)
let f be continuous Function of NTX,NTY; :: thesis: f .: (Cl A) c= Cl (f .: A)
now :: thesis: for o being object st o in f .: (Cl A) holds
o in Cl (f .: A)
let o be object ; :: thesis: ( o in f .: (Cl A) implies o in Cl (f .: A) )
assume o in f .: (Cl A) ; :: thesis: o in Cl (f .: A)
then consider x being object such that
A1: x in dom f and
A2: x in Cl A and
A3: o = f . x by FUNCT_1:def 6;
consider x9 being Point of NTX such that
A4: x = x9 and
A5: x9 is_adherent_point_of A by A2;
f . x in rng f by A1, FUNCT_1:3;
then reconsider y = f . x as Point of NTY ;
f is continuous ;
then y is_adherent_point_of f .: A by A4, A5, Lm12;
hence o in Cl (f .: A) by A3; :: thesis: verum
end;
hence f .: (Cl A) c= Cl (f .: A) ; :: thesis: verum