theorem Th13: :: SCMFSA8C:21

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) )