let m be Nat; :: thesis: for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & p1 ^ p2 = q1 ^ q2 holds
( p1 = q1 & p2 = q2 )
let p1, p2, q1, q2 be FinSequence; :: thesis: ( p1 is m -element & q1 is m -element & p1 ^ p2 = q1 ^ q2 implies ( p1 = q1 & p2 = q2 ) )
set P = p1 ^ p2;
set Q = q1 ^ q2;
assume ( p1 is m -element & q1 is m -element ) ; :: thesis: ( not p1 ^ p2 = q1 ^ q2 or ( p1 = q1 & p2 = q2 ) )
then reconsider x = p1, y = q1 as m -element FinSequence ;
( Seg (len p1) = dom p1 & Seg (len q1) = dom q1 ) by FINSEQ_1:def 3;
then A1: ( dom x = Seg m & dom y = Seg m ) by CARD_1:def 7;
assume A2: p1 ^ p2 = q1 ^ q2 ; :: thesis: ( p1 = q1 & p2 = q2 )
( x null 0 is Seg (m + 0) -defined & y null 0 is Seg (m + 0) -defined ) ;
then reconsider p11 = p1, q11 = q1 as Seg m -defined FinSequence ;
A3: p11 null (Seg m) = (q11 ^ q2) | (Seg m) by A1, A2, FINSEQ_6:11
.= q11 null (Seg m) by A1, FINSEQ_6:11 ;
hence p1 = q1 ; :: thesis: p2 = q2
thus p2 = q2 by A3, A2, FINSEQ_1:33; :: thesis: verum