let I be really-closed MacroInstruction of SCM+FSA ; :: thesis:
A1: dom (Macro (goto 0)) = {0,1} by COMPOS_1:61;
A2: ( 1 in dom (Macro (goto 0)) & 0 in dom (Macro (goto 0)) ) by COMPOS_1:60;
set F = Macro (goto 0);
Macro (goto 0) is really-closed

let l be Nat; :: according to AMISTD_1:def 9 :: thesis:
assume A3: l in dom (Macro (goto 0)) ; :: thesis:

per cases by A1, TARSKI:def 2;

suppose A4: l = 0 ; :: thesis:

then (Macro (goto 0)) /. l = (Macro (goto 0)) . l by A2, PARTFUN1:def 6
.= goto 0 by A4, COMPOS_1:58 ;
then NIC (((Macro (goto 0)) /. l),l) = {0} by SCMFSA10:33;
hence NIC (((Macro (goto 0)) /. l),l) c= dom (Macro (goto 0)) by A2, ZFMISC_1:31; :: thesis:

end;

suppose A5: l = 1 ; :: thesis:

then (Macro (goto 0)) /. l = (Macro (goto 0)) . l by A2, PARTFUN1:def 6
.= halt SCM+FSA by A5, COMPOS_1:59 ;
then NIC (((Macro (goto 0)) /. l),l) = {l} by AMISTD_1:2;
hence NIC (((Macro (goto 0)) /. l),l) c= dom (Macro (goto 0)) by A3, ZFMISC_1:31; :: thesis:

end;

end;

end;

then I ';' (Macro (goto 0)) is really-closed ;
hence I ';' (goto 0) is really-closed ; :: thesis: