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:47;
dom (fire e) c= Funcs P,NAT by Def9;
hence (fire e) * (id (Funcs P,NAT )) = fire e by A1, FUNCT_7:48; :: thesis: verum