consider fs1 being object such that
A1: fs1 in R1 by XBOOLE_0:def 1;
consider fs2 being object such that
A2: fs2 in R2 by XBOOLE_0:def 1;
reconsider fs1 = fs1, fs2 = fs2 as firing-sequence of N by A1, A2;
reconsider C = fs1 ^ fs2 as firing-sequence of N ;
A3: C = fs1 \/ ((len fs1) Shift fs2) by VALUED_1:49;
A4: fs1 misses (len fs1) Shift fs2 by VALUED_1:50;
A5: fs1 = Seq fs1 by FINSEQ_3:116;
Seq ((len fs1) Shift fs2) in R2 by A2, VALUED_1:46;
then C in R1 concur R2 by A1, A3, A4, A5;
hence not R1 concur R2 is empty ; :: thesis: verum