let P be set ; 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; for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)
let e1, e2 be Element of N; 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
by FINSEQ_1:61;
A5:
<*e1,e2*> . 1 = e1
by FINSEQ_1:61;
A6:
<*e1,e2*> . 2 = e2
by FINSEQ_1:61;
A7:
dom <*e1,e2*> = {1,2}
by A4, FINSEQ_1:4, FINSEQ_1:def 3;
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 A7, A8, PARTFUN1:def 8;
A11:
<*e1,e2*> /. 2 = <*e1,e2*> . 2
by A7, A9, PARTFUN1:def 8;
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 A2, A4, A12, 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, A13, FUNCT_7:53; verum