let T, S be non empty TopSpace; :: thesis: for f being Function of T,S
for P being Subset of T st P is compact & f is continuous holds
f .: P is compact
let f be Function of T,S; :: thesis: for P being Subset of T st P is compact & f is continuous holds
f .: P is compact
let P be Subset of T; :: thesis: ( P is compact & f is continuous implies f .: P is compact )
assume that
A1: P is compact and
A2: f is continuous ; :: thesis: f .: P is compact
P c= [#] T ;
then A3: P c= dom f by FUNCT_2:def 1;
for F0 being Subset-Family of S st F0 is Cover of f .: P & F0 is open holds
ex G being Subset-Family of S st
( G c= F0 & G is Cover of f .: P & G is finite )

proof

let F0 be Subset-Family of S; :: thesis: ( F0 is Cover of f .: P & F0 is open implies ex G being Subset-Family of S st
( G c= F0 & G is Cover of f .: P & G is finite ) )
assume that
A4: F0 is Cover of f .: P and
A5: F0 is open ; :: thesis: ex G being Subset-Family of S st
( G c= F0 & G is Cover of f .: P & G is finite )
set B0 = f " F0;
A6: f .: P c= union F0 by A4, SETFAM_1:def 11;
P c= union (f " F0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in union (f " F0) )
thus ( x in P implies x in union (f " F0) ) :: thesis: verum

proof

A7: f " (union F0) c= union (f " F0)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f " (union F0) or y in union (f " F0) )
assume A8: y in f " (union F0) ; :: thesis: y in union (f " F0)
thus y in union (f " F0) :: thesis: verum

proof

f . y in union F0 by A8, FUNCT_1:def 7;
then consider Q being set such that
A9: ( f . y in Q & Q in F0 ) by TARSKI:def 4;
A10: y in dom f by A8, FUNCT_1:def 7;
ex Z being set st
( y in Z & Z in f " F0 )

proof

set Z = f " Q;
take f " Q ; :: thesis: ( y in f " Q & f " Q in f " F0 )
thus ( y in f " Q & f " Q in f " F0 ) by A10, A9, FUNCT_1:def 7, FUNCT_2:def 9; :: thesis: verum

end;

hence y in union (f " F0) by TARSKI:def 4; :: thesis: verum

end;

end;

assume A11: x in P ; :: thesis: x in union (f " F0)
then A12: f . x in f .: P by A3, FUNCT_1:def 6;
reconsider x = x as Point of T by A11;
A13: f . x in union F0 by A6, A12;
A14: f " {(f . x)} c= f " (union F0)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f " {(f . x)} or y in f " (union F0) )
assume A15: y in f " {(f . x)} ; :: thesis: y in f " (union F0)
then f . y in {(f . x)} by FUNCT_1:def 7;
then A16: f . y in union F0 by A13, TARSKI:def 1;
y in dom f by A15, FUNCT_1:def 7;
hence y in f " (union F0) by A16, FUNCT_1:def 7; :: thesis: verum

end;

f . x in {(f . x)} by TARSKI:def 1;
then x in f " {(f . x)} by A3, A11, FUNCT_1:def 7;
then x in f " (union F0) by A14;
hence x in union (f " F0) by A7; :: thesis: verum

end;

end;

then A17: f " F0 is Cover of P by SETFAM_1:def 11;
f " F0 is open by A2, A5, Th4;
then ex B being Subset-Family of T st
( B c= f " F0 & B is Cover of P & B is finite ) by A1, A17, COMPTS_1:def 4;
then consider G being Subset-Family of S such that
A18: ( G c= F0 & G is Cover of f .: P & G is finite ) by Th7;
take G ; :: thesis: ( G c= F0 & G is Cover of f .: P & G is finite )
thus ( G c= F0 & G is Cover of f .: P & G is finite ) by A18; :: thesis: verum

end;

hence f .: P is compact by COMPTS_1:def 4; :: thesis: verum