let T be non empty TopSpace; :: thesis: for f being continuous RealMap of T
for A being compact Subset of T holds f .: A is compact
let f be continuous RealMap of T; :: thesis: for A being compact Subset of T holds f .: A is compact
let A be compact Subset of T; :: thesis: f .: A is compact
reconsider g = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
[#] (g .: A) is compact by WEIERSTR:9, WEIERSTR:13;
hence f .: A is compact by WEIERSTR:def 1; :: thesis: verum