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

proof

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

end;

consider F being Function of (bool ([#] T)),(bool ([#] S)) such that
A3: for x being Subset of ([#] T) holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
dom F = bool ([#] T) 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 .: P iff x in f .: P )

proof

let x be object ; :: thesis: ( x in F .: P iff x in f .: P )
thus ( x in F .: P implies x in f .: P ) :: thesis: ( x in f .: P implies x in F .: P )

proof

assume x in F .: P ; :: thesis: x in f .: P
then consider y being object such that
A4: y in dom F and
A5: ( y in P & x = F . y ) by FUNCT_1:def 6;
reconsider y = y as Subset of T by A4;
F . y = f .: y by A3;
hence x in f .: P by A5, FUNCT_2:def 10; :: thesis: verum

end;

thus ( x in f .: P implies x in F .: P ) :: thesis: verum

proof

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

end;

end;

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

proof

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

end;

hence f .: P is finite ; :: thesis: verum