let T, S be non empty TopSpace; :: thesis: for f being Function of T,S
for P being Subset of T
for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
let f be Function of T,S; :: thesis: for P being Subset of T
for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
let P be Subset of T; :: thesis: for F being Subset-Family of S st ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) holds
ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
let F be Subset-Family of S; :: thesis: ( ex B being Subset-Family of T st
( B c= f " F & B is Cover of P & B is finite ) implies ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) )
given B being Subset-Family of T such that A1: B c= f " F and
A2: B is Cover of P and
A3: B is finite ; :: thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
A4: P c= union B by A2, SETFAM_1:def 11;

now

per cases ( P <> {} or P = {} ) ;

case A5: P <> {} ; :: thesis: ( ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) & ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) )

thus ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) :: thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )

proof

consider s being FinSequence such that
A6: rng s = B by A3, FINSEQ_1:52;
B <> {} by A4, A5, ZFMISC_1:2;
then consider D being non empty set such that
A7: D = B ;
defpred S₁[ Element of D, Subset of ([#] S)] means for x being Element of D st $1 = x holds
for y being Subset of ([#] S) st $2 = y holds
( y in F & x = f " y );
A8: for x being Element of D ex y being Subset of ([#] S) st S₁[x,y]

proof

let x be Element of D; :: thesis: ex y being Subset of ([#] S) st S₁[x,y]
A9: x in B by A7;
then reconsider x = x as Subset of T ;
consider y being Subset of S such that
A10: ( y in F & x = f " y ) by A1, A9, FUNCT_2:def 9;
reconsider y = y as Subset of ([#] S) ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A10; :: thesis: verum

end;

consider F0 being Function of D,(bool ([#] S)) such that
A11: for x being Element of D holds S₁[x,F0 . x] from FUNCT_2:sch 3(A8);
A12: for x being Element of D holds
( F0 . x in F & x = f " (F0 . x) ) by A11;
reconsider F0 = F0 as Function of B,(bool ([#] S)) by A7;
A13: dom F0 = B by FUNCT_2:def 1;
then reconsider q = F0 * s as FinSequence by A6, FINSEQ_1:16;
set G = rng q;
A14: rng q c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in F )
assume x in rng q ; :: thesis: x in F
then consider y being set such that
A15: ( y in dom q & x = q . y ) by FUNCT_1:def 3;
( s . y in B & x = F0 . (s . y) ) by A13, A15, FUNCT_1:11, FUNCT_1:12;
hence x in F by A7, A12; :: thesis: verum

end;

then reconsider G = rng q as Subset-Family of S by XBOOLE_1:1;
reconsider G = G as Subset-Family of S ;
take G ; :: thesis: ( G c= F & G is Cover of f .: P & G is finite )
for x being set st x in f .: P holds
x in union G

proof

let x be set ; :: thesis: ( x in f .: P implies x in union G )
assume A16: x in f .: P ; :: thesis: x in union G
ex A being set st
( x in A & A in G )

proof

consider y being set such that
A17: y in dom f and
A18: y in P and
A19: x = f . y by A16, FUNCT_1:def 6;
consider C being set such that
A20: y in C and
A21: C in B by A4, A18, TARSKI:def 4;
C = f " (F0 . C) by A7, A12, A21;
then A22: x in f .: (f " (F0 . C)) by A17, A19, A20, FUNCT_1:def 6;
set A = F0 . C;
take F0 . C ; :: thesis: ( x in F0 . C & F0 . C in G )
( f .: (f " (F0 . C)) c= F0 . C & G = rng F0 ) by A6, A13, FUNCT_1:75, RELAT_1:28;
hence ( x in F0 . C & F0 . C in G ) by A21, A22, FUNCT_2:4; :: thesis: verum

end;

hence x in union G by TARSKI:def 4; :: thesis: verum

end;

then f .: P c= union G by TARSKI:def 3;
hence ( G c= F & G is Cover of f .: P & G is finite ) by A14, SETFAM_1:def 11; :: thesis: verum

end;

hence ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ; :: thesis: verum

end;

case A23: P = {} ; :: thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )

ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )

proof

set G = {} ;
reconsider G = {} as Subset-Family of S by XBOOLE_1:2;
reconsider G = G as Subset-Family of S ;
take G ; :: thesis: ( G c= F & G is Cover of f .: P & G is finite )
f .: P = {}

proof

assume f .: P <> {} ; :: thesis: contradiction
then consider x being set such that
A24: x in f .: P by XBOOLE_0:def 1;
ex z being set st
( z in dom f & z in P & x = f . z ) by A24, FUNCT_1:def 6;
hence contradiction by A23; :: thesis: verum

end;

hence ( G c= F & G is Cover of f .: P & G is finite ) by SETFAM_1:def 11, XBOOLE_1:2, ZFMISC_1:2; :: thesis: verum

end;

hence ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ; :: thesis: verum

end;

end;

end;

hence ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite ) ; :: thesis: verum