let il be Instruction-Location of SCM+FSA ; :: thesis: Next il = NextLoc il
Next il = il. SCM+FSA ,((locnum il) + 1)

proof

Next (il. SCM+FSA ,(locnum il)) = il. SCM+FSA ,((locnum il) + 1) by Th87;
hence Next il = il. SCM+FSA ,((locnum il) + 1) by AMISTD_1:def 13; :: thesis: verum

end;

hence Next il = NextLoc il ; :: thesis: verum