let p, r, q be XFinSequence; :: 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

assume A3: p ^ r = q ^ r ; :: thesis: p = q
then (len p) + (len r) = len (q ^ r) by Def4;
then B4: (len p) + (len r) = (len q) + (len r) by Def4;
for k being Element of NAT st k in dom p holds
p . k = q . k

proof

let k be Element of 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, Def4
.= q . k by B4, A5, Def4 ;
:: thesis: verum

end;

hence p = q by B4, Th10; :: thesis: verum

end;

now

assume A6: r ^ p = r ^ q ; :: thesis: p = q
then B7: (len r) + (len p) = len (r ^ q) by Def4
.= (len r) + (len q) by Def4 ;
for k being Element of NAT st k in dom p holds
p . k = q . k

proof

let k be Element of 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, Def4
.= q . k by B7, A8, Def4 ;
:: thesis: verum

end;

hence p = q by B7, Th10; :: thesis: verum

end;

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