let T be TopStruct ; :: thesis: for P being Subset of T

for S being non empty TopStruct

for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds

f .: P is compact

let P be Subset of T; :: thesis: for S being non empty TopStruct

for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds

f .: P is compact

let S be non empty TopStruct ; :: thesis: for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds

f .: P is compact

let f be Function of T,S; :: thesis: ( f is continuous & rng f = [#] S & P is compact implies f .: P is compact )

assume that

A1: f is continuous and

A2: rng f = [#] S and

A3: P is compact ; :: thesis: f .: P is compact

let F be Subset-Family of S; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of f .: P & F is open implies ex G being Subset-Family of S st

( G c= F & G is Cover of f .: P & G is finite ) )

assume that

A4: F is Cover of f .: P and

A5: F is open ; :: thesis: ex G being Subset-Family of S st

( G c= F & G is Cover of f .: P & G is finite )

reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:42;

f .: P c= union F by A4, SETFAM_1:def 11;

then A6: f " (f .: P) c= f " (union F) by RELAT_1:143;

P c= [#] T ;

then P c= dom f by FUNCT_2:def 1;

then A7: P c= f " (f .: P) by FUNCT_1:76;

union G = f " (union F) by A2, FUNCT_3:26;

then P c= union G by A6, A7;

then A8: G is Cover of P by SETFAM_1:def 11;

G is open by A1, A5, TOPS_2:47;

then consider G9 being Subset-Family of T such that

A9: G9 c= G and

A10: G9 is Cover of P and

A11: G9 is finite by A3, A8;

reconsider F9 = (.: f) .: G9 as Subset-Family of S ;

take F9 ; :: thesis: ( F9 c= F & F9 is Cover of f .: P & F9 is finite )

A12: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75;

(.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:29, RELAT_1:123;

then A13: (.: f) .: G c= F by A12;

(.: f) .: G9 c= (.: f) .: G by A9, RELAT_1:123;

hence F9 c= F by A13; :: thesis: ( F9 is Cover of f .: P & F9 is finite )

A14: P c= union G9 by A10, SETFAM_1:def 11;

dom f = [#] T by FUNCT_2:def 1;

then union F9 = f .: (union G9) by FUNCT_3:14;

then f .: P c= union F9 by A14, RELAT_1:123;

hence F9 is Cover of f .: P by SETFAM_1:def 11; :: thesis: F9 is finite

thus F9 is finite by A11; :: thesis: verum

for S being non empty TopStruct

for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds

f .: P is compact

let P be Subset of T; :: thesis: for S being non empty TopStruct

for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds

f .: P is compact

let S be non empty TopStruct ; :: thesis: for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds

f .: P is compact

let f be Function of T,S; :: thesis: ( f is continuous & rng f = [#] S & P is compact implies f .: P is compact )

assume that

A1: f is continuous and

A2: rng f = [#] S and

A3: P is compact ; :: thesis: f .: P is compact

let F be Subset-Family of S; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of f .: P & F is open implies ex G being Subset-Family of S st

( G c= F & G is Cover of f .: P & G is finite ) )

assume that

A4: F is Cover of f .: P and

A5: F is open ; :: thesis: ex G being Subset-Family of S st

( G c= F & G is Cover of f .: P & G is finite )

reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:42;

f .: P c= union F by A4, SETFAM_1:def 11;

then A6: f " (f .: P) c= f " (union F) by RELAT_1:143;

P c= [#] T ;

then P c= dom f by FUNCT_2:def 1;

then A7: P c= f " (f .: P) by FUNCT_1:76;

union G = f " (union F) by A2, FUNCT_3:26;

then P c= union G by A6, A7;

then A8: G is Cover of P by SETFAM_1:def 11;

G is open by A1, A5, TOPS_2:47;

then consider G9 being Subset-Family of T such that

A9: G9 c= G and

A10: G9 is Cover of P and

A11: G9 is finite by A3, A8;

reconsider F9 = (.: f) .: G9 as Subset-Family of S ;

take F9 ; :: thesis: ( F9 c= F & F9 is Cover of f .: P & F9 is finite )

A12: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75;

(.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:29, RELAT_1:123;

then A13: (.: f) .: G c= F by A12;

(.: f) .: G9 c= (.: f) .: G by A9, RELAT_1:123;

hence F9 c= F by A13; :: thesis: ( F9 is Cover of f .: P & F9 is finite )

A14: P c= union G9 by A10, SETFAM_1:def 11;

dom f = [#] T by FUNCT_2:def 1;

then union F9 = f .: (union G9) by FUNCT_3:14;

then f .: P c= union F9 by A14, RELAT_1:123;

hence F9 is Cover of f .: P by SETFAM_1:def 11; :: thesis: F9 is finite

thus F9 is finite by A11; :: thesis: verum