let P be set ; :: thesis: for m being marking of P
for t2, t1 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
let m be marking of P; :: thesis: for t2, t1 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
let t2, t1 be transition of P; :: thesis: fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
dom (fire t1) = Funcs (P,NAT) by Def9;
then A1: m in dom (fire t1) by FUNCT_2:8;
thus fire (t2,(fire (t1,m))) = (fire t2) . (fire (t1,m)) by Def9
.= (fire t2) . ((fire t1) . m) by Def9
.= ((fire t2) * (fire t1)) . m by A1, FUNCT_1:13 ; :: thesis: verum