let N be with_zero set ; :: thesis: for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))}
let l be Element of NAT ; :: thesis: 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 ; :: thesis: verum