theorem :: AMI_2:27

dom (SCM-VAL * SCM-OK) = SCM-Memory by Lm5;