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 TOPMETR:24, TOPREAL6:83;
[#] (g .: A) is compact by WEIERSTR:15, WEIERSTR:19;
hence f .: A is compact by WEIERSTR:def 3; :: thesis: verum