let P be set ; 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; for e being Element of N holds fire <*e*> = fire e
let e be Element of N; 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; verum