deffunc H₁( Function) -> set = dom $1;
let V be set ; :: thesis: 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 ; :: thesis: 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)); :: thesis: Involved A is finite
defpred S₁[ set ] means ( $1 in A & $1 is finite );
defpred S₂[ set ] means $1 in A;
set X = { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ;
A1: for x being set st x in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } holds
x is finite

proof

let x be set ; :: thesis: ( x in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } implies x is finite )
assume x in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ; :: thesis: x is finite
then ex f1 being Element of PFuncs (V,C) st
( x = dom f1 & f1 in A & f1 is finite ) ;
hence x is finite ; :: thesis: verum

end;

A2: A is finite ;
A3: { H₁(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 { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ) )

proof

let x be object ; :: thesis: ( x in Involved A iff ex Y being set st
( x in Y & Y in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ) )

hereby :: thesis: ( ex Y being set st
( x in Y & Y in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ) implies x in Involved A )

assume x in Involved A ; :: thesis: ex Y being set st
( x in Y & Y in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } )
then consider f being finite Function such that
A4: f in A and
A5: x in dom f by Def1;
A c= PFuncs (V,C) by FINSUB_1:def 5;
then dom f in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } by A4;
hence ex Y being set st
( x in Y & Y in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ) by A5; :: thesis: verum

end;

given Y being set such that A6: x in Y and
A7: Y in { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } ; :: thesis: x in Involved A
ex f1 being Element of PFuncs (V,C) st
( Y = dom f1 & f1 in A & f1 is finite ) by A7;
hence x in Involved A by A6, Def1; :: thesis: verum

end;

then A8: Involved A = union { H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } by TARSKI:def 4;
A9: for g being Element of PFuncs (V,C) st S₁[g] holds
S₂[g] ;
{ H₁(f) where f is Element of PFuncs (V,C) : S₁[f] } c= { H₁(f) where f is Element of PFuncs (V,C) : S₂[f] } from FRAENKEL:sch 1(A9);
hence Involved A is finite by A3, A8, A1, FINSET_1:7; :: thesis: verum