let I, J be MacroInstruction of SCM+FSA ; :: thesis: for n being Nat st n < LastLoc I holds
(I ";" J) . n = I . n
let l be Nat; :: thesis: ( l < LastLoc I implies (I ";" J) . l = I . l )
assume A1: l < LastLoc I ; :: thesis: (I ";" J) . l = I . l
LastLoc I in dom I by VALUED_1:30;
then A2: l in dom I by A1, AFINSQ_1:def 12;
then I . l <> halt SCM+FSA by A1, COMPOS_1:def 15;
hence (I ";" J) . l = I . l by A2, Th5; :: thesis: verum