for P being set
for N being Petri_net of P
for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )