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

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