theorem Th2: :: SCMFSA8C:2

for I, J being Program of SCM+FSA
for k being Nat st card I <= k & k < (card I) + (card J) holds
for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds
(I ";" J) . k = IncAddr (i,(card I))