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 & B is Cover of P & B is finite ) ; :: thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of f .: P & G is finite )
A2: P c= union B by A1, SETFAM_1:def 12;

now

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

case A3: 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

B <> {} by A2, A3, ZFMISC_1:2;
then consider D being non empty set such that
A4: 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 );
A5: 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]
A6: x in B by A4;
then reconsider x = x as Subset of T ;
consider y being Subset of S such that
A7: ( y in F & x = f " y ) by A1, A6, FUNCT_2:def 10;
reconsider y = y as Subset of ([#] S) ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A7; :: thesis: verum

end;

consider F0 being Function of D,(bool ([#] S)) such that
A8: for x being Element of D holds S₁[x,F0 . x] from FUNCT_2:sch 3(A5);
A9: for x being Element of D holds
( F0 . x in F & x = f " (F0 . x) ) by A8;
reconsider F0 = F0 as Function of B,(bool ([#] S)) by A4;
consider s being FinSequence such that
A10: rng s = B by A1, FINSEQ_1:73;
A11: dom F0 = B by FUNCT_2:def 1;
then reconsider q = F0 * s as FinSequence by A10, FINSEQ_1:20;
set G = rng q;
A12: 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
A13: ( y in dom q & x = q . y ) by FUNCT_1:def 5;
A14: s . y in B by A11, A13, FUNCT_1:21;
x = F0 . (s . y) by A13, FUNCT_1:22;
hence x in F by A4, A9, A14; :: 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 )
G is Cover of f .: P

proof

f .: P c= union G

proof

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 A15: 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
A16: ( y in dom f & y in P & x = f . y ) by A15, FUNCT_1:def 12;
consider C being set such that
A17: ( y in C & C in B ) by A2, A16, TARSKI:def 4;
( F0 . C in F & C = f " (F0 . C) ) by A4, A9, A17;
then A18: x in f .: (f " (F0 . C)) by A16, A17, FUNCT_1:def 12;
A19: f .: (f " (F0 . C)) c= F0 . C by FUNCT_1:145;
A20: G = rng F0 by A10, A11, RELAT_1:47;
set A = F0 . C;
take F0 . C ; :: thesis: ( x in F0 . C & F0 . C in G )
thus ( x in F0 . C & F0 . C in G ) by A17, A18, A19, A20, FUNCT_2:6; :: thesis: verum

end;

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

end;

hence f .: P c= union G by TARSKI:def 3; :: thesis: verum

end;

hence G is Cover of f .: P by SETFAM_1:def 12; :: thesis: verum

end;

hence ( G c= F & G is Cover of f .: P & G is finite ) by A12, FINSEQ_1:73; :: 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 A21: 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 = {} ;
A22: f .: P = {}

proof

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

end;

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 )
thus ( G c= F & G is Cover of f .: P & G is finite ) by A22, SETFAM_1:def 12, 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