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 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 A4, FINSEQ_1:2, 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 6;
A11:
<*e1,e2*> /. 2 = <*e1,e2*> . 2
by A7, A9, PARTFUN1:def 6;
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:44;
(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 A1, A13, FUNCT_7:51; verum