let p1, q1, r1, p2, q2, r2 be FinSequence; :: thesis: ( len p1 = len p2 & len q1 = len q2 & (p1 ^ q1) ^ r1 = (p2 ^ q2) ^ r2 implies ( p1 = p2 & q1 = q2 & r1 = r2 ) )
assume A1: ( len p1 = len p2 & len q1 = len q2 & (p1 ^ q1) ^ r1 = (p2 ^ q2) ^ r2 ) ; :: thesis: ( p1 = p2 & q1 = q2 & r1 = r2 )
A2: p1 ^ (q1 ^ r1) = (p1 ^ q1) ^ r1 by FINSEQ_1:32
.= p2 ^ (q2 ^ r2) by A1, FINSEQ_1:32 ;
then ( p1 c= p1 ^ (q1 ^ r1) & p2 c= p1 ^ (q1 ^ r1) ) by FINSEQ_6:10;
hence p1 = p2 by A1, FINSEQ_2:129; :: thesis: ( q1 = q2 & r1 = r2 )
then A3: q1 ^ r1 = q2 ^ r2 by A2, FINSEQ_1:33;
( q1 c= q1 ^ r1 & q2 c= q2 ^ r2 ) by FINSEQ_6:10;
hence q1 = q2 by A1, A3, FINSEQ_2:129; :: thesis: r1 = r2
hence r1 = r2 by A3, FINSEQ_1:33; :: thesis: verum