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