:: deftheorem defines Values MEMSTR_0:def 5 :
for N being with_zero set
for S being non empty Mem-Struct over N
for o being Object of S holds Values o = (the_Values_of S) . o;