let I be MacroInstruction of SCM+FSA ; :: thesis: for i being No-StopCode Instruction of SCM+FSA
for n being Nat st n + 1 < card I holds
I +* (n,i) is MacroInstruction of SCM+FSA
let i be No-StopCode Instruction of SCM+FSA; :: thesis: for n being Nat st n + 1 < card I holds
I +* (n,i) is MacroInstruction of SCM+FSA
let n be Nat; :: thesis: ( n + 1 < card I implies I +* (n,i) is MacroInstruction of SCM+FSA )
assume A1: n + 1 < card I ; :: thesis: I +* (n,i) is MacroInstruction of SCM+FSA
set F = I +* (n,i);
A2: dom (I +* (n,i)) = dom I by FUNCT_7:30;
then A3: LastLoc (I +* (n,i)) = LastLoc I ;
A4: n + 1 < card (I +* (n,i)) by A1, A2;
A5: card (I +* (n,i)) >= 0 + 1 by NAT_1:13;
LastLoc (I +* (n,i)) = (card (I +* (n,i))) -' 1 by AFINSQ_1:70
.= (card (I +* (n,i))) - 1 by A5, XREAL_1:233 ;
then (n + 1) - 1 < LastLoc (I +* (n,i)) by A4, XREAL_1:14;
then n < LastLoc I by A3;
then (I +* (n,i)) . (LastLoc (I +* (n,i))) = I . (LastLoc I) by A3, FUNCT_7:32
.= halt SCM+FSA by COMPOS_1:def 14 ;
then A6: I +* (n,i) is halt-ending ;
I +* (n,i) is unique-halt

proof

let f be Nat; :: according to COMPOS_1:def 15 :: thesis: ( not (I +* (n,i)) . f = halt SCM+FSA or not f in dom (I +* (n,i)) or f = LastLoc (I +* (n,i)) )
assume that
A7: (I +* (n,i)) . f = halt SCM+FSA and
A8: f in dom (I +* (n,i)) ; :: thesis: f = LastLoc (I +* (n,i))

now :: thesis: not I . f <> halt SCM+FSA

assume A9: I . f <> halt SCM+FSA ; :: thesis: contradiction

per cases ( f = n or f <> n ) ;

suppose f = n ; :: thesis: contradiction

then (I +* (n,i)) . f = i by FUNCT_7:31, A8, A2;
hence contradiction by A7, COMPOS_0:def 12; :: thesis: verum

end;

suppose f <> n ; :: thesis: contradiction

then (I +* (n,i)) . f = I . f by FUNCT_7:32;
hence contradiction by A9, A7; :: thesis: verum

end;

end;

end;

hence f = LastLoc (I +* (n,i)) by A2, A8, A3, COMPOS_1:def 15; :: thesis: verum

end;

hence I +* (n,i) is MacroInstruction of SCM+FSA by A6; :: thesis: verum