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: (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;
A2: { (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 } = { (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

thus { (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 ) } :: according to XBOOLE_0:def 10 :: thesis: { (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 ) } 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 }

proof

let z be set ; :: 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 consider f1 being Element of PFuncs A,B such that
A3: ( z = union { ((f1 . i) \ i) where i is Element of PFuncs V,C : i in A } & dom f1 = A ) ;
thus 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 ) } by A3; :: thesis: verum

end;

thus { (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 ) } 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 } :: thesis: verum

proof

let z be set ; :: 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 : ( f in 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 : 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 : ( f in 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 : dom f = A }
then consider f1 being Element of PFuncs A,B such that
A4: ( z = union { ((f1 . i) \ i) where i is Element of PFuncs V,C : i in A } & f1 in PFuncs A,B & dom f1 = A ) ;
thus 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 } by A4; :: thesis: verum

end;

end;

reconsider PF = PFuncs A,B as functional non empty finite set by Th5;
deffunc H₁( Element of PF) -> set = union { (($1 . i) \ i) where i is Element of PFuncs V,C : i in A } ;
defpred S₁[ Element of PF] means ( $1 in PFuncs A,B & dom $1 = A );
{ H₁(f) where f is Element of PF : S₁[f] } is finite from PRE_CIRC:sch 1();
then (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 finite by A2;
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, FINSUB_1:def 5; :: thesis: verum