theorem Th45: :: SCMFSA_2:52

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;