let p be FinSequence; :: thesis:
let x be object ; :: thesis:
assume that
A1: p is one-to-one and
A2: x in rng p ; :: thesis:
set q = p - {x};
let k be Nat; :: thesis:
assume A3: k in dom (p - {x}) ; :: thesis:
A4: p just_once_values x by A1, A2, Th8;
then ( dom (p - {x}) = Seg (len (p - {x})) & len (p - {x}) = (len p) - 1 ) by Th30, FINSEQ_1:def 3;
then k <= (len p) - 1 by A3, FINSEQ_1:1;
then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, XREAL_1:19;
then k + 1 in Seg (len p) ;
then A5: ( dom (p - {x}) c= dom p & k + 1 in dom p ) by FINSEQ_1:def 3, FINSEQ_3:63;
thus ( (p - {x}) . k = p . k implies k < x .. p ) :: thesis:

assume that
A6: (p - {x}) . k = p . k and
A7: not k < x .. p ; :: thesis:
(p - {x}) . k = p . (k + 1) by A4, A3, A7, Th31;
then k + 0 = k + 1 by A1, A3, A5, A6;
hence contradiction ; :: thesis:

end;

thus ( k < x .. p implies (p - {x}) . k = p . k ) by A4, A3, Th31; :: thesis:
thus ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) :: thesis:

assume A8: (p - {x}) . k = p . (k + 1) ; :: thesis:
assume not x .. p <= k ; :: thesis:
then p . (k + 1) = p . k by A4, A3, A8, Th31;
then k + 0 = k + 1 by A1, A3, A5;
hence contradiction ; :: thesis:

end;

thus ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) by A4, A3, Th31; :: thesis: