let P be Subset of (TOP-REAL 2); :: thesis: ( P is Bounded implies for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P) )
assume A1: P is Bounded ; :: thesis: for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P)
let g be continuous RealMap of (TOP-REAL 2); :: thesis: Cl (g .: P) c= g .: (Cl P)
reconsider f = g as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
A2: f is continuous by Th83;
Cl P is compact by A1, Th71, Th88;
then f .: (Cl P) is closed by A2, COMPTS_1:16, WEIERSTR:15;
then A3: g .: (Cl P) is closed by Th79;
g .: P c= g .: (Cl P) by PRE_TOPC:48, RELAT_1:156;
hence Cl (g .: P) c= g .: (Cl P) by A3, PSCOMP_1:32; :: thesis: verum