for z being Nat
for N being with_zero set
for l being Nat st l = z holds
SUCC (l,(STC N)) = {z,(z + 1)}