let N be non empty with_non-empty_elements 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 natural number such that
A1: l = il. (STC N),k by Th26;
A2: k = locnum l,(STC N) by A1, Def13;
thus SUCC l,(STC N) = {k,(k + 1)} by A1, Th24, Th37
.= {k,(il. (STC N),(k + 1))} by Th37
.= {l,(NextLoc l,(STC N))} by A1, A2, Th37 ; :: thesis: verum