theorem Th3: :: SFMASTR1:4

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