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 ;
TARSKI:def 3 ( 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 }
;
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 ) }
;
verum
end;
defpred S1[ Element of PF] means ( $1 in PFuncs (A,B) & dom $1 = A );
deffunc H1( Element of PF) -> set = union { (($1 . i) \ i) where i is Element of PFuncs (V,C) : i in A } ;
A2:
{ H1(f) where f is Element of PF : S1[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; verum