:: deftheorem defines mi SUBSTLAT:def 2 :
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;