let p, r, q be XFinSequence; :: thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )

A1: now :: thesis: ( p ^ r = q ^ r & ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )

assume A2: p ^ r = q ^ r ; :: thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
then (len p) + (len r) = len (q ^ r) by Def3;
then A3: (len p) + (len r) = (len q) + (len r) 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 A4: k in dom p ; :: thesis: p . k = q . k
hence p . k = (q ^ r) . k by A2, Def3
.= q . k by A3, A4, Def3 ;
:: thesis: verum

end;

hence ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q ) by A3, Th8; :: thesis: verum

end;

A5: now :: thesis: ( r ^ p = r ^ q & ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )

assume A6: r ^ p = r ^ q ; :: thesis: ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q )
then A7: (len r) + (len p) = len (r ^ q) by Def3
.= (len r) + (len 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, Def3
.= q . k by A7, A8, Def3 ;
:: thesis: verum

end;

hence ( ( p ^ r = q ^ r or r ^ p = r ^ q ) implies p = q ) by A7, Th8; :: thesis: verum

end;

assume ( p ^ r = q ^ r or r ^ p = r ^ q ) ; :: thesis: p = q
hence p = q by A1, A5; :: thesis: verum