theorem Th14: :: SCMFSA6B:16

for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of st P +* I halts_on s holds
for J being Program of
for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)