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

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