deffunc H1( Function) -> set = dom $1;
let V be set ; for C being finite set
for A being non empty Element of Fin (PFuncs (V,C)) holds Involved A is finite
let C be finite set ; for A being non empty Element of Fin (PFuncs (V,C)) holds Involved A is finite
let A be non empty Element of Fin (PFuncs (V,C)); Involved A is finite
defpred S1[ set ] means ( $1 in A & $1 is finite );
defpred S2[ set ] means $1 in A;
set X = { H1(f) where f is Element of PFuncs (V,C) : S1[f] } ;
A1:
for x being set st x in { H1(f) where f is Element of PFuncs (V,C) : S1[f] } holds
x is finite
A2:
A is finite
;
A3:
{ H1(f) where f is Element of PFuncs (V,C) : f in A } is finite
from FRAENKEL:sch 21(A2);
for x being object holds
( x in Involved A iff ex Y being set st
( x in Y & Y in { H1(f) where f is Element of PFuncs (V,C) : S1[f] } ) )
then A8:
Involved A = union { H1(f) where f is Element of PFuncs (V,C) : S1[f] }
by TARSKI:def 4;
A9:
for g being Element of PFuncs (V,C) st S1[g] holds
S2[g]
;
{ H1(f) where f is Element of PFuncs (V,C) : S1[f] } c= { H1(f) where f is Element of PFuncs (V,C) : S2[f] }
from FRAENKEL:sch 1(A9);
hence
Involved A is finite
by A3, A8, A1, FINSET_1:7; verum