not j destroysdestroy intloc 0 by Def6;
then reconsider Mj = Macro j as good Program of SCM+FSA by SCMFSA8C:99;
not i destroysdestroy intloc 0 by Def6;
then reconsider Mi = Macro i as good Program of SCM+FSA by SCMFSA8C:99;
Mi ';' Mj is good ;
hence i ';' j is good ; :: thesis: verum