:: deftheorem Def8 defines fire PNPROC_1:def 8 :
for P being set
for t being transition of P
for b₃ being Function holds
( b₃ = fire t iff ( dom b₃ = Funcs (P,NAT) & ( for m being marking of P holds b₃ . m = fire (t,m) ) ) );