let TS be TopSpace; :: thesis: for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds
for PS being Subset of TS st PS is closed holds
f .: PS is closed
let SS be non empty TopSpace; :: thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds
for PS being Subset of TS st PS is closed holds
f .: PS is closed
let f be Function of TS,SS; :: thesis: ( TS is compact & SS is T_2 & rng f = [#] SS & f is continuous implies for PS being Subset of TS st PS is closed holds
f .: PS is closed )
assume that
A1: TS is compact and
A2: SS is T_2 and
A3: rng f = [#] SS and
A4: f is continuous ; :: thesis: for PS being Subset of TS st PS is closed holds
f .: PS is closed
let PS be Subset of TS; :: thesis: ( PS is closed implies f .: PS is closed )
assume PS is closed ; :: thesis: f .: PS is closed
then PS is compact by A1, Th8;
hence f .: PS is closed by A2, A3, A4, Th7, Th15; :: thesis: verum