let P be set ; :: thesis: for N being Petri_net of P
for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)

let N be Petri_net of P; :: thesis: for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)
let e1, e2 be Element of N; :: thesis: fire <*e1,e2*> = (fire e2) * (fire e1)
consider F being Function-yielding FinSequence such that
A1: fire <*e1,e2*> = compose (F,(Funcs (P,NAT))) and
A2: len F = len <*e1,e2*> and
A3: for i being Element of NAT st i in dom <*e1,e2*> holds
F . i = fire (<*e1,e2*> /. i) by Def10;
A4: len <*e1,e2*> = 2 by FINSEQ_1:44;
A5: <*e1,e2*> . 1 = e1 by FINSEQ_1:44;
A6: <*e1,e2*> . 2 = e2 by FINSEQ_1:44;
A7: dom <*e1,e2*> = {1,2} by ;
A8: 1 in {1,2} by TARSKI:def 2;
A9: 2 in {1,2} by TARSKI:def 2;
A10: <*e1,e2*> /. 1 = <*e1,e2*> . 1 by ;
A11: <*e1,e2*> /. 2 = <*e1,e2*> . 2 by ;
A12: F . 1 = fire e1 by A3, A5, A7, A8, A10;
F . 2 = fire e2 by A3, A6, A7, A9, A11;
then A13: F = <*(fire e1),(fire e2)*> by ;
(fire e1) * (id (Funcs (P,NAT))) = fire e1 by Th24;
then ((fire e2) * (fire e1)) * (id (Funcs (P,NAT))) = (fire e2) * (fire e1) by RELAT_1:36;
hence fire <*e1,e2*> = (fire e2) * (fire e1) by ; :: thesis: verum