for G being non empty 1-sorted
for i being Element of SCM-Memory st i in SCM-Data-Loc holds
((SCM-VAL G) * SCM-OK) . i = the carrier of G