let p be FinSequence; :: thesis: for x being object st p just_once_values x holds
for k being Nat st k in dom (p - {x}) holds
( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )
let x be object ; :: thesis: ( p just_once_values x implies for k being Nat st k in dom (p - {x}) holds
( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) )
assume A1: p just_once_values x ; :: thesis: for k being Nat st k in dom (p - {x}) holds
( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )
set q = p - {x};
let k be Nat; :: thesis: ( k in dom (p - {x}) implies ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) )
assume A2: k in dom (p - {x}) ; :: thesis: ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )
set A = { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } ;
A3: dom (p - {x}) c= dom p by FINSEQ_3:63;
thus ( k < x .. p implies (p - {x}) . k = p . k ) :: thesis: ( x .. p <= k implies (p - {x}) . k = p . (k + 1) )

proof

assume A4: k < x .. p ; :: thesis: (p - {x}) . k = p . k
{ L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } or y in {} )
assume y in { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } ; :: thesis: y in {}
then consider L being Element of NAT such that
y = L and
A5: ( L in dom p & L <= k ) and
A6: p . L in {x} ;
p . L <> x by A1, A4, A5, Th26;
hence y in {} by A6, TARSKI:def 1; :: thesis: verum

end;

then A7: { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } = {} ;
p . k <> x by A1, A2, A3, A4, Th26;
then not p . k in {x} by TARSKI:def 1;
then (p - {x}) . (k - 0) = p . k by A2, A3, A7, CARD_1:27, FINSEQ_3:85;
hence (p - {x}) . k = p . k ; :: thesis: verum

end;

set B = { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } ;
assume A8: x .. p <= k ; :: thesis: (p - {x}) . k = p . (k + 1)
A9: x in rng p by A1, Th5;
A10: { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } = {(x .. p)}

proof

thus { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } c= {(x .. p)} :: according to XBOOLE_0:def 10 :: thesis: {(x .. p)} c= { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } or y in {(x .. p)} )
assume y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } ; :: thesis: y in {(x .. p)}
then consider M being Element of NAT such that
A11: M = y and
A12: M in dom p and
M <= k + 1 and
A13: p . M in {x} ;
p . M = x by A13, TARSKI:def 1;
then M = x .. p by A1, A12, Th26;
hence y in {(x .. p)} by A11, TARSKI:def 1; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {(x .. p)} or y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } )
assume y in {(x .. p)} ; :: thesis: y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) }
then A14: y = x .. p by TARSKI:def 1;
p . (x .. p) = x by A9, Th19;
then A15: p . (x .. p) in {x} by TARSKI:def 1;
( x .. p in dom p & x .. p <= k + 1 ) by A9, A8, Th20, NAT_1:12;
hence y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } by A14, A15; :: thesis: verum

end;

then reconsider B = { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } as finite set ;
( dom (p - {x}) = Seg (len (p - {x})) & len (p - {x}) = (len p) - 1 ) by A1, Th30, FINSEQ_1:def 3;
then k <= (len p) - 1 by A2, 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 A16: k + 1 in dom p by FINSEQ_1:def 3;

now :: thesis: not p . (k + 1) in {x}

x .. p <> k + 1 by A8, XREAL_1:29;
then A17: p . (k + 1) <> x by A1, A16, Th26;
assume p . (k + 1) in {x} ; :: thesis: contradiction
hence contradiction by A17, TARSKI:def 1; :: thesis: verum

end;

then (p - {x}) . ((k + 1) - (card B)) = p . (k + 1) by A16, FINSEQ_3:85;
then (p - {x}) . ((k + 1) - 1) = p . (k + 1) by A10, CARD_1:30;
hence (p - {x}) . k = p . (k + 1) ; :: thesis: verum