let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: I ';' (goto 0) is really-closed
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

proof

let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not l in K543(NAT,(Macro (goto 0))) or NIC (((Macro (goto 0)) /. l),l) c= K543(NAT,(Macro (goto 0))) )
assume A3: l in dom (Macro (goto 0)) ; :: thesis: NIC (((Macro (goto 0)) /. l),l) c= K543(NAT,(Macro (goto 0)))

per cases then ( l = 0 or l = 1 ) by A1, TARSKI:def 2;

suppose A4: l = 0 ; :: thesis: NIC (((Macro (goto 0)) /. l),l) c= K543(NAT,(Macro (goto 0)))

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: verum

end;

suppose A5: l = 1 ; :: thesis: NIC (((Macro (goto 0)) /. l),l) c= K543(NAT,(Macro (goto 0)))

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: verum

end;

end;

end;

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