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