let PTN be Petri_net; :: thesis: 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; :: thesis: for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
let t be transition of PTN; :: thesis: 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 ; :: thesis: verum