let P be set ; :: thesis: for N being Petri_net of P

for e being Element of N holds fire <*e*> = fire e

let N be Petri_net of P; :: thesis: for e being Element of N holds fire <*e*> = fire e

let e be Element of N; :: thesis: fire <*e*> = fire e

consider F being Function-yielding FinSequence such that

A1: fire <*e*> = compose (F,(Funcs (P,NAT))) and

A2: len F = len <*e*> and

A3: for i being Element of NAT st i in dom <*e*> holds

F . i = fire (<*e*> /. i) by Def10;

A4: len <*e*> = 1 by FINSEQ_1:40;

A5: <*e*> . 1 = e by FINSEQ_1:40;

dom <*e*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then A6: 1 in dom <*e*> by TARSKI:def 1;

then A7: <*e*> /. 1 = <*e*> . 1 by PARTFUN1:def 6;

F . 1 = fire (<*e*> /. 1) by A3, A6;

then A8: F = <*(fire e)*> by A2, A4, A5, A7, FINSEQ_1:40;

dom (fire e) c= Funcs (P,NAT) by Def8;

hence fire <*e*> = fire e by A1, A8, FUNCT_7:46; :: thesis: verum

for e being Element of N holds fire <*e*> = fire e

let N be Petri_net of P; :: thesis: for e being Element of N holds fire <*e*> = fire e

let e be Element of N; :: thesis: fire <*e*> = fire e

consider F being Function-yielding FinSequence such that

A1: fire <*e*> = compose (F,(Funcs (P,NAT))) and

A2: len F = len <*e*> and

A3: for i being Element of NAT st i in dom <*e*> holds

F . i = fire (<*e*> /. i) by Def10;

A4: len <*e*> = 1 by FINSEQ_1:40;

A5: <*e*> . 1 = e by FINSEQ_1:40;

dom <*e*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then A6: 1 in dom <*e*> by TARSKI:def 1;

then A7: <*e*> /. 1 = <*e*> . 1 by PARTFUN1:def 6;

F . 1 = fire (<*e*> /. 1) by A3, A6;

then A8: F = <*(fire e)*> by A2, A4, A5, A7, FINSEQ_1:40;

dom (fire e) c= Funcs (P,NAT) by Def8;

hence fire <*e*> = fire e by A1, A8, FUNCT_7:46; :: thesis: verum