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 Def11;
A4: ( len <*e1,e2*> = 2 & <*e1,e2*> . 1 = e1 & <*e1,e2*> . 2 = e2 ) by FINSEQ_1:61;
then A5: dom <*e1,e2*> = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
A6: ( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then A7: ( <*e1,e2*> /. 1 = <*e1,e2*> . 1 & <*e1,e2*> /. 2 = <*e1,e2*> . 2 ) by A5, PARTFUN1:def 8;
then A8: F . 1 = fire e1 by A3, A4, A5, A6;
F . 2 = fire e2 by A3, A4, A5, A6, A7;
then A9: F = <*(fire e1),(fire e2)*> by A2, A4, A8, FINSEQ_1:61;
(fire e1) * (id (Funcs P,NAT )) = fire e1 by Th38;
then ((fire e2) * (fire e1)) * (id (Funcs P,NAT )) = (fire e2) * (fire e1) by RELAT_1:55;
hence fire <*e1,e2*> = (fire e2) * (fire e1) by A1, A9, FUNCT_7:53; :: thesis: verum