theorem :: SCMFSA_1:33

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