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 Def10;
F = {} by A2;
hence fire (<*> N) = id (Funcs (P,NAT)) by A1, FUNCT_7:39; :: thesis: verum