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:56, FINSEQ_4:25;
A2: <*(Firing (<*t*> /. 1),M0)*> /. 1 = Firing (<*t*> /. 1),M0 by FINSEQ_4:25;

A3: now

A4: len <*t*> = 0 + 1 by FINSEQ_1:56;
let i be Element of 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:56
.= len <*(Firing (<*t*> /. 1),M0)*> by FINSEQ_1:56 ;
hence Firing t,M0 = Firing <*t*>,M0 by A1, A2, A3, Def5; :: thesis: verum