theorem Th7: :: SCMFSA_1:17

for s being SCM+FSA-State
for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State