deffunc H1( 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 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
proof
let x be set ; :: thesis: ( x in { H1(f) where f is Element of PFuncs (V,C) : S1[f] } implies x is finite )
assume x in { H1(f) where f is Element of PFuncs (V,C) : S1[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: { 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] } ) )
proof
let x be object ; :: thesis: ( 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] } ) )
hereby :: thesis: ( ex Y being set st
( x in Y & Y in { H1(f) where f is Element of PFuncs (V,C) : S1[f] } ) implies x in Involved A )
assume x in Involved A ; :: thesis: ex Y being set st
( x in Y & Y in { H1(f) where f is Element of PFuncs (V,C) : S1[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 { H1(f) where f is Element of PFuncs (V,C) : S1[f] } by A4;
hence ex Y being set st
( x in Y & Y in { H1(f) where f is Element of PFuncs (V,C) : S1[f] } ) by A5; :: thesis: verum
end;
given Y being set such that A6: x in Y and
A7: Y in { H1(f) where f is Element of PFuncs (V,C) : S1[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 { 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; :: thesis: verum