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

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