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 A2: m in dom (fire t1) by FUNCT_2:11;
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 A2, FUNCT_1:23 ; :: thesis: verum