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
deffunc H₁( Function) -> set = dom $1;
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 g being Element of PFuncs V,C st S₁[g] holds
S₂[g] ;
A2: { 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(A1);
A3: A is finite ;
A4: { H₁(f) where f is Element of PFuncs V,C : f in A } is finite from FRAENKEL:sch 21(A3);
for x being set 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 set ; :: 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
A5: ( f in A & 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 A5;
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 & Y in { H₁(f) where f is Element of PFuncs V,C : S₁[f] } ) ; :: thesis: x in Involved A
consider f1 being Element of PFuncs V,C such that
A7: ( Y = dom f1 & f1 in A & f1 is finite ) by A6;
thus x in Involved A by A6, A7, 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;
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 consider f1 being Element of PFuncs V,C such that
A10: ( x = dom f1 & f1 in A & f1 is finite ) ;
thus x is finite by A10; :: thesis: verum

end;

hence Involved A is finite by A8, A2, A4, FINSET_1:25; :: thesis: verum