theorem :: AMI_2:28

for s being SCM-State holds dom s = SCM-Memory by Lm5, CARD_3:9;