let P be set ; :: thesis: for N being Petri_net of P
for e being Element of N
for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
let N be Petri_net of P; :: thesis: for e being Element of N
for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
let e be Element of N; :: thesis: for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
let C be firing-sequence of N; :: thesis: fire (C ^ <*e*>) = (fire e) * (fire C)
fire (C ^ <*e*>) = (fire <*e*>) * (fire C) by Th27;
hence fire (C ^ <*e*>) = (fire e) * (fire C) by Th23; :: thesis: verum