for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory holds
s = s +* S by FUNCT_4:75;