let p, q, r be FinSequence; :: thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
assume A1: ( p ^ r = q ^ r or r ^ p = r ^ q ) ; :: thesis: p = q

A2: now :: thesis: ( p ^ r = q ^ r implies p = q )

assume A3: p ^ r = q ^ r ; :: thesis: p = q
then (len p) + (len r) = len (q ^ r) by Th22;
then (len p) + (len r) = (len q) + (len r) by Th22;
then A4: dom p = Seg (len q) by Def3
.= dom q by Def3 ;
for k being Nat st k in dom p holds
p . k = q . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = q . k )
assume A5: k in dom p ; :: thesis: p . k = q . k
hence p . k = (q ^ r) . k by A3, Def7
.= q . k by A4, A5, Def7 ;
:: thesis: verum

end;

hence p = q by A4; :: thesis: verum

end;

now :: thesis: ( r ^ p = r ^ q implies p = q )

assume A6: r ^ p = r ^ q ; :: thesis: p = q
then (len r) + (len p) = len (r ^ q) by Th22
.= (len r) + (len q) by Th22 ;
then A7: dom p = Seg (len q) by Def3
.= dom q by Def3 ;
for k being Nat st k in dom p holds
p . k = q . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = q . k )
assume A8: k in dom p ; :: thesis: p . k = q . k
hence p . k = (r ^ q) . ((len r) + k) by A6, Def7
.= q . k by A7, A8, Def7 ;
:: thesis: verum

end;

hence p = q by A7; :: thesis: verum

end;

hence p = q by A1, A2; :: thesis: verum