theorem Th24: :: PNPROC_1:24

for P being set
for N being Petri_net of P
for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e