let I, J be really-closed MacroInstruction of SCM+FSA ; :: thesis: ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is really-closed
A1: ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) = (J ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= J ";" (((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA)) by SCMFSA6A:25 ;
((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) is really-closed by SCMFSA_X:28;
hence ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is really-closed by A1; :: thesis: verum