let P be set ; :: thesis: for N being Petri_net of P
for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

let N be Petri_net of P; :: thesis: for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)
let C1, C2 be firing-sequence of N; :: thesis: fire (C1 ^ C2) = (fire C2) * (fire C1)
consider F being Function-yielding FinSequence such that
A1: fire (C1 ^ C2) = compose (F,(Funcs (P,NAT))) and
A2: len F = len (C1 ^ C2) and
A3: for i being Element of NAT st i in dom (C1 ^ C2) holds
F . i = fire ((C1 ^ C2) /. i) by Def10;
consider F1 being Function-yielding FinSequence such that
A4: fire C1 = compose (F1,(Funcs (P,NAT))) and
A5: len F1 = len C1 and
A6: for i being Element of NAT st i in dom C1 holds
F1 . i = fire (C1 /. i) by Def10;
consider F2 being Function-yielding FinSequence such that
A7: fire C2 = compose (F2,(Funcs (P,NAT))) and
A8: len F2 = len C2 and
A9: for i being Element of NAT st i in dom C2 holds
F2 . i = fire (C2 /. i) by Def10;
A10: rng (fire C1) c= Funcs (P,NAT) by Th26;
len F = (len C1) + (len C2) by ;
then A11: dom F = Seg ((len F1) + (len F2)) by ;
A12: for k being Nat st k in dom F1 holds
F . k = F1 . k
proof
let k be Nat; :: thesis: ( k in dom F1 implies F . k = F1 . k )
assume A13: k in dom F1 ; :: thesis: F . k = F1 . k
A14: dom F1 = Seg (len F1) by FINSEQ_1:def 3;
A15: dom F1 = Seg (len C1) by ;
A16: dom F1 = dom C1 by ;
A17: k in dom C1 by ;
A18: dom C1 c= dom (C1 ^ C2) by FINSEQ_1:26;
then A19: F . k = fire ((C1 ^ C2) /. k) by ;
A20: (C1 ^ C2) /. k = (C1 ^ C2) . k by ;
A21: (C1 ^ C2) . k = C1 . k by ;
C1 . k = C1 /. k by ;
hence F . k = F1 . k by A6, A13, A16, A19, A20, A21; :: thesis: verum
end;
for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . k
proof
let k be Nat; :: thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume A22: k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k
dom F2 = Seg (len F2) by FINSEQ_1:def 3;
then A23: dom F2 = dom C2 by ;
then A24: (len F1) + k in dom (C1 ^ C2) by ;
reconsider lFk = (len F1) + k as Element of NAT by ORDINAL1:def 12;
A25: F . ((len F1) + k) = fire ((C1 ^ C2) /. lFk) by ;
A26: (C1 ^ C2) /. ((len F1) + k) = (C1 ^ C2) . ((len F1) + k) by ;
A27: (C1 ^ C2) . ((len F1) + k) = C2 . k by ;
C2 . k = C2 /. k by ;
hence F . ((len F1) + k) = F2 . k by A9, A22, A23, A25, A26, A27; :: thesis: verum
end;
then F = F1 ^ F2 by ;
hence fire (C1 ^ C2) = (fire C2) * (fire C1) by ; :: thesis: verum