theorem Th9: :: SCMPDS_7:11

for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being State of SCMPDS
for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )