theorem Th15: :: SCMFSA8C:23

for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2