let R be good Ring; :: thesis: for il being Instruction-Location of SCM R holds Next il = NextLoc il
let il be Instruction-Location of SCM R; :: thesis: Next il = NextLoc il
Next il = il. (SCM R),((locnum il) + 1)

proof

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

end;

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