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