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 Def11;
A4: ( len <*e*> = 1 & <*e*> . 1 = e ) by FINSEQ_1:57;
dom <*e*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then A5: 1 in dom <*e*> by TARSKI:def 1;
then A6: <*e*> /. 1 = <*e*> . 1 by PARTFUN1:def 8;
F . 1 = fire (<*e*> /. 1) by A3, A5;
then A7: F = <*(fire e)*> by A2, A4, A6, FINSEQ_1:57;
dom (fire e) c= Funcs P,NAT by Def9;
hence fire <*e*> = fire e by A1, A7, FUNCT_7:48; :: thesis: verum