set i = SubFrom a,(intloc 0 );
reconsider Mi = Macro (SubFrom a,(intloc 0 )) as good Program of SCM+FSA by SCMFSA7B:14, SCMFSA8C:99;
I ';' Mi is good ;
then reconsider Ii = I ';' (SubFrom a,(intloc 0 )) as good Program of SCM+FSA ;
if>0 a,(loop (if=0 a,(Goto (insloc 2)),Ii)),(Stop SCM+FSA ) is good ;
hence Times a,I is good ; :: thesis: verum