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

proof

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

end;

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

proof

assume A9: (p - {x}) . k = p . (k + 1) ; :: thesis:
assume not x .. p <= k ; :: thesis:
then p . (k + 1) = p . k by A3, A4, A9, Th41;
then k + 0 = k + 1 by A1, A4, A5, A6, FUNCT_1:def 8;
hence contradiction ; :: thesis:

end;

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