theorem :: SCMFSA9A:21

for p1, p2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)