let T, S be non empty TopSpace; :: thesis:
let f be Function of T,S; :: thesis:
let P be Subset of T; :: thesis:
assume that
A1: P is compact and
A2: f is continuous ; :: thesis:
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 )

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

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

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 )

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

end;

end;

assume A11: x in P ; :: thesis:
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)

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:
thus ( G c= F0 & G is Cover of f .: P & G is finite ) by A18; :: thesis:

end;