theorem Th2: :: AMI_2:7

for i being Element of SCM-Memory st i in SCM-Data-Loc holds
(SCM-VAL * SCM-OK) . i = INT