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