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 set ; :: 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 consider B being Element of Fin (PFuncs V,C) such that
A1: ( 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 ) ) ;
thus x in Fin (PFuncs V,C) by A1; :: 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