theorem :: AMI_2:29

for S being SCM-State holds S is SCM-Memory -defined total Function ;