let P be set ; :: thesis: for N being Petri_net of P holds fire (<*> N) = id (Funcs P,NAT )
let N be Petri_net of P; :: thesis: fire (<*> N) = id (Funcs P,NAT )
consider F being Function-yielding FinSequence such that
A1: fire (<*> N) = compose F,(Funcs P,NAT ) and
A2: len F = len (<*> N) and
for i being Element of NAT st i in dom (<*> N) holds
F . i = fire ((<*> N) /. i) by Def11;
F = {} by A2;
hence fire (<*> N) = id (Funcs P,NAT ) by A1, FUNCT_7:41; :: thesis: verum