let PTN be Petri_net; for M0 being marking of PTN
for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
let M0 be marking of PTN; for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
let t be transition of PTN; Firing (t,M0) = Firing (<*t*>,M0)
set Q = <*t*>;
consider M being FinSequence of nat_marks_of PTN such that
A1:
( len <*t*> = len M & Firing (<*t*>,M0) = M /. (len M) & M /. 1 = Firing ((<*t*> /. 1),M0) & ( for i being Nat st i < len <*t*> & i > 0 holds
M /. (i + 1) = Firing ((<*t*> /. (i + 1)),(M /. i)) ) )
by Defb;
thus Firing (<*t*>,M0) =
Firing ((<*t*> /. 1),M0)
by A1, FINSEQ_1:39
.=
Firing (t,M0)
by FINSEQ_4:16
; verum