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 )
defpred S₁[ Subset of ([#] S), Subset of ([#] T)] means for s, t being set st $1 = s & $2 = t holds
t = f " s;
assume Q is finite ; :: thesis: f " Q is finite
then consider s being FinSequence such that
A1: rng s = Q by FINSEQ_1:52;
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);
dom F = bool ([#] S) by FUNCT_2:def 1;
then reconsider q = F * s as FinSequence by A1, FINSEQ_1:16;
for x being object holds
( x in F .: Q iff x in f " Q )

proof

let x be object ; :: thesis: ( x in F .: Q iff x in f " Q )
A4: dom F = bool ([#] S) by FUNCT_2:def 1;
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 object such that
A5: y in dom F and
A6: ( y in Q & x = F . y ) by FUNCT_1:def 6;
reconsider y = y as Subset of S by A5;
F . y = f " y by A3;
hence x in f " Q by A6, FUNCT_2:def 9; :: thesis: verum

end;

assume A7: 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
A8: y in Q and
A9: x = f " y by A7, FUNCT_2:def 9;
x = F . y by A3, A9;
hence x in F .: Q by A8, A4, FUNCT_1:def 6; :: thesis: verum

end;

then A10: F .: Q = f " Q by TARSKI:2;
ex q being FinSequence st rng q = f " Q

proof

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

end;

hence f " Q is finite ; :: thesis: verum