for s being natural Number holds s ! is Element of NAT