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