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

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

S is compact

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

S is compact

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

assume A1: T is compact ; :: thesis: ( not f is continuous or not rng f = [#] S or S is compact )

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

then A2: [#] T c= f " (f .: ([#] T)) by FUNCT_1:76;

assume that

A3: f is continuous and

A4: rng f = [#] S ; :: thesis: S is compact

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

( G c= F & G is Cover of S & G is finite ) )

assume that

A5: F is Cover of S and

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

( G c= F & G is Cover of S & G is finite )

set F1 = F;

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

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

.= f " (rng f) by A4, A5, SETFAM_1:45

.= f " (f .: (dom f)) by RELAT_1:113

.= f " (f .: ([#] T)) by FUNCT_2:def 1 ;

then A7: G is Cover of T by A2, SETFAM_1:def 11;

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

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

then A9: (.: f) .: G c= F by A8;

G is open by A3, A6, TOPS_2:47;

then consider G9 being Subset-Family of T such that

A10: G9 c= G and

A11: G9 is Cover of T and

A12: G9 is finite by A1, A7;

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

take F9 ; :: thesis: ( F9 c= F & F9 is Cover of S & F9 is finite )

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

hence F9 c= F by A9; :: thesis: ( F9 is Cover of S & F9 is finite )

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

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

.= f .: ([#] T) by A11, SETFAM_1:45

.= f .: (dom f) by FUNCT_2:def 1

.= [#] S by A4, RELAT_1:113 ;

hence F9 is Cover of S by SETFAM_1:def 11; :: thesis: F9 is finite

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

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

S is compact

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

S is compact

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

assume A1: T is compact ; :: thesis: ( not f is continuous or not rng f = [#] S or S is compact )

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

then A2: [#] T c= f " (f .: ([#] T)) by FUNCT_1:76;

assume that

A3: f is continuous and

A4: rng f = [#] S ; :: thesis: S is compact

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

( G c= F & G is Cover of S & G is finite ) )

assume that

A5: F is Cover of S and

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

( G c= F & G is Cover of S & G is finite )

set F1 = F;

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

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

.= f " (rng f) by A4, A5, SETFAM_1:45

.= f " (f .: (dom f)) by RELAT_1:113

.= f " (f .: ([#] T)) by FUNCT_2:def 1 ;

then A7: G is Cover of T by A2, SETFAM_1:def 11;

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

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

then A9: (.: f) .: G c= F by A8;

G is open by A3, A6, TOPS_2:47;

then consider G9 being Subset-Family of T such that

A10: G9 c= G and

A11: G9 is Cover of T and

A12: G9 is finite by A1, A7;

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

take F9 ; :: thesis: ( F9 c= F & F9 is Cover of S & F9 is finite )

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

hence F9 c= F by A9; :: thesis: ( F9 is Cover of S & F9 is finite )

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

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

.= f .: ([#] T) by A11, SETFAM_1:45

.= f .: (dom f) by FUNCT_2:def 1

.= [#] S by A4, RELAT_1:113 ;

hence F9 is Cover of S by SETFAM_1:def 11; :: thesis: F9 is finite

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