theorem Th16: :: SCMBSORT:26

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