let T, S be non empty TopSpace; :: thesis: for f being Function of T,S
for Q being Subset-Family of S st Q is finite holds
f " Q is finite
let f be Function of T,S; :: thesis: for Q being Subset-Family of S st Q is finite holds
f " Q is finite
let Q be Subset-Family of S; :: thesis: ( Q is finite implies f " Q is finite )
assume Q is finite ; :: thesis: f " Q is finite
then consider s being FinSequence such that
A1: rng s = Q by FINSEQ_1:73;
defpred S₁[ Subset of ([#] S), Subset of ([#] T)] means for s, t being set st $1 = s & $2 = t holds
t = f " s;
A2: for x being Subset of ([#] S) ex y being Subset of ([#] T) st S₁[x,y]

proof

let x be Subset of ([#] S); :: thesis: ex y being Subset of ([#] T) st S₁[x,y]
reconsider x = x as set ;
set y = f " x;
reconsider y = f " x as Subset of ([#] T) ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider F being Function of (bool ([#] S)),(bool ([#] T)) such that
A3: for x being Subset of ([#] S) holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
( Q c= bool ([#] S) & dom F = bool ([#] S) ) by FUNCT_2:def 1;
then reconsider q = F * s as FinSequence by A1, FINSEQ_1:20;
A4: F .: Q = f " Q

proof

for x being set holds
( x in F .: Q iff x in f " Q )

proof

let x be set ; :: thesis: ( x in F .: Q iff x in f " Q )
thus ( x in F .: Q implies x in f " Q ) :: thesis: ( x in f " Q implies x in F .: Q )

proof

assume x in F .: Q ; :: thesis: x in f " Q
then consider y being set such that
A5: ( y in dom F & y in Q & x = F . y ) by FUNCT_1:def 12;
reconsider y = y as Subset of S by A5;
F . y = f " y by A3;
hence x in f " Q by A5, FUNCT_2:def 10; :: thesis: verum

end;

assume A6: x in f " Q ; :: thesis: x in F .: Q
then reconsider x = x as Subset of T ;
consider y being Subset of S such that
A7: ( y in Q & x = f " y ) by A6, FUNCT_2:def 10;
A8: x = F . y by A3, A7;
dom F = bool ([#] S) by FUNCT_2:def 1;
hence x in F .: Q by A7, A8, FUNCT_1:def 12; :: thesis: verum

end;

hence F .: Q = f " Q by TARSKI:2; :: thesis: verum

end;

ex q being FinSequence st rng q = f " Q

proof

take q ; :: thesis: rng q = f " Q
thus rng q = f " Q by A1, A4, RELAT_1:160; :: thesis: verum

end;

hence f " Q is finite by FINSEQ_1:73; :: thesis: verum