let il be Element of NAT ; :: thesis: succ il = NextLoc il,SCM+FSA
succ (il. SCM+FSA ,(locnum il,SCM+FSA )) = il. SCM+FSA ,((locnum il,SCM+FSA ) + 1) by Th87;
hence succ il = NextLoc il,SCM+FSA by AMISTD_1:def 13; :: thesis: verum