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

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