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 " () by
.= f " (rng f) by
.= f " (f .: (dom f)) by RELAT_1:113
.= f " (f .: ([#] T)) by FUNCT_2:def 1 ;
then A7: G is Cover of T by ;
A8: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75;
(.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by ;
then A9: (.: f) .: G c= F by A8;
G is open by ;
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 ;
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
.= f .: (dom f) by FUNCT_2:def 1
.= [#] S by ;
hence F9 is Cover of S by SETFAM_1:def 11; :: thesis: F9 is finite
thus F9 is finite by A12; :: thesis: verum