theorem Th63: :: SCMFSA8C:72

for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )