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

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