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

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