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 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; :: thesis: verum

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 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; :: thesis: verum