set IT = { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ;
{ A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } c= Fin (PFuncs (V,C))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } or x in Fin (PFuncs (V,C)) )
assume x in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } ; :: thesis: x in Fin (PFuncs (V,C))
then ex B being Element of Fin (PFuncs (V,C)) st
( B = x & ( for u being set st u in B holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in B & t in B & s c= t holds
s = t ) ) ;
hence x in Fin (PFuncs (V,C)) ; :: thesis: verum

end;

hence { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } is Subset of (Fin (PFuncs (V,C))) ; :: thesis: verum