:: deftheorem Def10 defines fire PNPROC_1:def 10 :
for P being set
for N being Petri_net of P
for C being firing-sequence of N
for b₄ being Function holds
( b₄ = fire C iff ex F being Function-yielding FinSequence st
( b₄ = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) );