let R be good Ring; :: thesis: for il being Element of NAT holds succ il = NextLoc il,(SCM R)
let il be Element of NAT ; :: thesis: succ il = NextLoc il,(SCM R)
succ (il. (SCM R),(locnum il,(SCM R))) = il. (SCM R),((locnum il,(SCM R)) + 1) by Th67;
hence succ il = NextLoc il,(SCM R) by AMISTD_1:def 13; :: thesis: verum