let q, r be FinSequence; :: thesis: ( len q = (len p) - (x .. p) & ( for k being Nat st k in dom q holds
q . k = p . (k + (x .. p)) ) & len r = (len p) - (x .. p) & ( for k being Nat st k in dom r holds
r . k = p . (k + (x .. p)) ) implies q = r )
assume that
A3: len q = (len p) - (x .. p) and
A4: for k being Nat st k in dom q holds
q . k = p . (k + (x .. p)) ; :: thesis: ( not len r = (len p) - (x .. p) or ex k being Nat st
( k in dom r & not r . k = p . (k + (x .. p)) ) or q = r )
assume that
A5: len r = (len p) - (x .. p) and
A6: for k being Nat st k in dom r holds
r . k = p . (k + (x .. p)) ; :: thesis: q = r

now :: thesis: for k being Nat st k in dom q holds
q . k = r . k

let k be Nat; :: thesis: ( k in dom q implies q . k = r . k )
A7: ( dom q = Seg (len q) & dom r = Seg (len r) ) by FINSEQ_1:def 3;
assume A8: k in dom q ; :: thesis: q . k = r . k
then q . k = p . (k + (x .. p)) by A4;
hence q . k = r . k by A3, A5, A6, A8, A7; :: thesis: verum

end;

hence q = r by A3, A5, FINSEQ_2:9; :: thesis: verum