for z being Nat
for N being with_zero set holds il. ((STC N),z) = z