theorem :: PNPROC_1:21

for P being set
for m being marking of P
for t1, t2 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m