let m be Nat; for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds
( p1 = q1 & p2 = q2 )
let p1, p2, q1, q2 be FinSequence; ( p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) implies ( p1 = q1 & p2 = q2 ) )
set m1 = len p1;
set m2 = len p2;
set n1 = len q1;
set n2 = len q2;
assume
( p1 is m -element & q1 is m -element )
; ( ( not p1 ^ p2 = q1 ^ q2 & not p2 ^ p1 = q2 ^ q1 ) or ( p1 = q1 & p2 = q2 ) )
then reconsider p11 = p1, q11 = q1 as m -element FinSequence ;
reconsider p22 = p2 null p2 as len p2 -element FinSequence ;
reconsider q22 = q2 null q2 as len q2 -element FinSequence ;
set PA = p11 ^ p22;
set PB = p22 ^ p11;
set QA = q11 ^ q22;
set QB = q22 ^ q11;
A1:
( len (p11 ^ p22) = m + (len p2) & len (p22 ^ p11) = (len p2) + m & len (q11 ^ q22) = m + (len q2) & len (q22 ^ q11) = (len q2) + m )
by CARD_1:def 7;
assume A2:
( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 )
; ( p1 = q1 & p2 = q2 )
then A3:
( p11 ^ p22 = q11 ^ q22 or p22 ^ p11 = q22 ^ q11 )
;
reconsider q22 = q22 as len p2 -element FinSequence by A2, A1;
( p22 is len p2 -element & q22 is len p2 -element )
;
hence
( p1 = q1 & p2 = q2 )
by A3, Lm49; verum