for PTN being Petri_net
for M0 being Boolean_marking of PTN
for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)