theorem Th8: :: SCMFSA6B:8

for P1, P2 being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being really-closed parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )