theorem Th17: :: AMI_WSTD:17

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