theorem :: MEMSTR_0:77

for N being with_zero set
for A being non empty with_non-empty_values Mem-Struct over N
for s being State of A
for o being Object of A holds s . o in Values o