theorem Th5: :: SCMFSA6A:15

for I, J being Program of
for l being Nat st l in dom I & I . l <> halt SCM+FSA holds
(I ";" J) . l = I . l