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