for P being set
for t being transition of P holds rng (fire t) c= Funcs (P,NAT)