let T, S be non empty TopSpace; 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; for P being Subset-Family of T st P is finite holds
f .: P is finite
let P be Subset-Family of T; ( P is finite implies f .: P is finite )
defpred S1[ 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
; 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 S1[x,y]
proof
let x be
Subset of
([#] T);
ex y being Subset of ([#] S) st S1[x,y]
reconsider x =
x as
set ;
set y =
f .: x;
reconsider y =
f .: x as
Subset of
([#] S) ;
take
y
;
S1[x,y]
thus
S1[
x,
y]
;
verum
end;
consider F being Function of (bool ([#] T)),(bool ([#] S)) such that
A3:
for x being Subset of ([#] T) holds S1[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 )
then A10:
F .: P = f .: P
by TARSKI:2;
ex q being FinSequence st rng q = f .: P
hence
f .: P is finite
; verum