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