:: deftheorem defines SubstitutionSet SUBSTLAT:def 1 :
for V, C being set holds SubstitutionSet (V,C) = { 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 ) ) } ;