for PTN being Petri_net
for M0 being marking of PTN
for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))