theorem :: PNPROC_1:22

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