reconsider PF = PFuncs (A,B) as functional non empty finite set by PRE_POLY:17;
set Z = { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;
set K = (PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;
A1: { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } c= { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A ) }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } or z in { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A ) } )
assume z in { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ; :: thesis: z in { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A ) }
then ex f1 being Element of PFuncs (A,B) st
( z = union { ((f1 . i) \ i) where i is Element of PFuncs (V,C) : i in A } & dom f1 = A ) ;
hence z in { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : ( f in PFuncs (A,B) & dom f = A ) } ; :: thesis: verum

end;

defpred S₁[ Element of PF] means ( $1 in PFuncs (A,B) & dom $1 = A );
deffunc H₁( Element of PF) -> set = union { (($1 . i) \ i) where i is Element of PFuncs (V,C) : i in A } ;
A2: { H₁(f) where f is Element of PF : S₁[f] } is finite from PRE_CIRC:sch 1();
(PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } c= PFuncs (V,C) by XBOOLE_1:17;
hence (PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } is Element of Fin (PFuncs (V,C)) by A1, A2, FINSUB_1:def 5; :: thesis: verum