let S, T be non empty TopStruct ; :: thesis: for f being Function of S,T
for A being Subset of T st f is being_homeomorphism & A is compact holds
f " A is compact
let f be Function of S,T; :: thesis: for A being Subset of T st f is being_homeomorphism & A is compact holds
f " A is compact
let A be Subset of T; :: thesis: ( f is being_homeomorphism & A is compact implies f " A is compact )
assume that
A1: f is being_homeomorphism and
A2: A is compact ; :: thesis: f " A is compact
A3: ( rng f = [#] T & f is one-to-one ) by A1, TOPS_2:def 5;
f " is being_homeomorphism by A1, TOPS_2:56;
then A4: rng (f ") = [#] S by TOPS_2:def 5;
f " is continuous by A1, TOPS_2:def 5;
then (f ") .: A is compact by A2, A4, COMPTS_1:15;
hence f " A is compact by A3, TOPS_2:55; :: thesis: verum