theorem :: SCMFSA8A:43

for I being MacroInstruction of SCM+FSA
for k being Nat holds (Goto k) ";" I = (Macro (goto k)) ';' I