let PTN be PT_net_Str ; :: 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
A1: ( len <*t*> = 1 & len {} = 0 ) by FINSEQ_1:56;
set M = <*(Firing (<*t*> /. 1),M0)*>;
A2: len <*t*> = 1 by FINSEQ_1:56
.= len <*(Firing (<*t*> /. 1),M0)*> by FINSEQ_1:56 ;
A3: <*t*> /. 1 = t by FINSEQ_4:25;
A4: <*(Firing (<*t*> /. 1),M0)*> /. 1 = Firing (<*t*> /. 1),M0 by FINSEQ_4:25;

now

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 A5: ( i < len <*t*> & i > 0 ) ; :: thesis: <*(Firing (<*t*> /. 1),M0)*> /. (i + 1) = Firing (<*t*> /. (i + 1)),(<*(Firing (<*t*> /. 1),M0)*> /. i)
len <*t*> = 0 + 1 by FINSEQ_1:56;
hence <*(Firing (<*t*> /. 1),M0)*> /. (i + 1) = Firing (<*t*> /. (i + 1)),(<*(Firing (<*t*> /. 1),M0)*> /. i) by A5, NAT_1:13; :: thesis: verum

end;

hence Firing t,M0 = Firing <*t*>,M0 by A1, A2, A3, A4, Def5; :: thesis: verum