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 7 :: 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:54;
f .: P c= union F by A4, SETFAM_1:def 12;
then A6: f " (f .: P) c= f " (union F) by RELAT_1:178;
P c= [#] T ;
then P c= dom f by FUNCT_2:def 1;
then A7: P c= f " (f .: P) by FUNCT_1:146;
union G = f " (union F) by A2, FUNCT_3:30;
then P c= union G by A6, A7, XBOOLE_1:1;
then A8: G is Cover of P by SETFAM_1:def 12;
G is open by A1, A5, TOPS_2:59;
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, Def7;
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:145;
(.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:33, RELAT_1:156;
then A13: (.: f) .: G c= F by A12, XBOOLE_1:1;
(.: f) .: G9 c= (.: f) .: G by A9, RELAT_1:156;
hence F9 c= F by A13, XBOOLE_1:1; :: thesis: ( F9 is Cover of f .: P & F9 is finite )
A14: P c= union G9 by A10, SETFAM_1:def 12;
dom f = [#] T by FUNCT_2:def 1;
then union F9 = f .: (union G9) by FUNCT_3:16;
then f .: P c= union F9 by A14, RELAT_1:156;
hence F9 is Cover of f .: P by SETFAM_1:def 12; :: thesis: F9 is finite
thus F9 is finite by A11; :: thesis: verum