let PTN be Petri_net; :: thesis: for M0 being Boolean_marking of PTN
for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
let M0 be Boolean_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 M = <*(Firing ((<*t*> /. 1),M0))*>;
A1: ( len <*t*> = 1 & <*t*> /. 1 = t ) by FINSEQ_1:39, FINSEQ_4:16;
A2: <*(Firing ((<*t*> /. 1),M0))*> /. 1 = Firing ((<*t*> /. 1),M0) by FINSEQ_4:16;

A3: now :: thesis: for i being Nat st i < len <*t*> & i > 0 holds
<*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i))

A4: len <*t*> = 0 + 1 by FINSEQ_1:39;
let i be Nat; :: thesis: ( i < len <*t*> & i > 0 implies <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) )
assume ( i < len <*t*> & i > 0 ) ; :: thesis: <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i))
hence <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) by A4, NAT_1:13; :: thesis: verum

end;

len <*t*> = 1 by FINSEQ_1:39
.= len <*(Firing ((<*t*> /. 1),M0))*> by FINSEQ_1:39 ;
hence Firing (t,M0) = Firing (<*t*>,M0) by A1, A2, A3, Def5; :: thesis: verum