theorem :: SCMFSA6A:41

for I, J being MacroInstruction of SCM+FSA
for n being Nat st n < LastLoc I holds
(I ";" J) . n = I . n