let P be set ; :: thesis: for N being Petri_net of P
for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e
let N be Petri_net of P; :: thesis: for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e
let e be Element of N; :: thesis: (fire e) * (id (Funcs (P,NAT))) = fire e
A1: compose (<*(fire e)*>,(Funcs (P,NAT))) = (fire e) * (id (Funcs (P,NAT))) by FUNCT_7:45;
dom (fire e) c= Funcs (P,NAT) by Def8;
hence (fire e) * (id (Funcs (P,NAT))) = fire e by A1, FUNCT_7:46; :: thesis: verum