let N be with_zero set ; for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))}
let l be Element of NAT ; SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))}
set M = STC N;
consider k being Nat such that
A1:
l = il. ((STC N),k)
by Th6;
A2:
k = locnum (l,(STC N))
by A1, Def5;
thus SUCC (l,(STC N)) =
{k,(k + 1)}
by A1, Th17, AMISTD_1:8
.=
{k,(il. ((STC N),(k + 1)))}
by Th17
.=
{l,(NextLoc (l,(STC N)))}
by A1, A2, Th17
; verum