:: deftheorem defines FinPartSt MEMSTR_0:def 16 :
for N being with_zero set
for S being with_non-empty_values Mem-Struct over N holds FinPartSt S = { p where p is Element of sproduct (the_Values_of S) : p is finite } ;