let p be FinSequence; :: thesis: for x being set 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 set ; :: 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:70;
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 set ; :: 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, Th36;
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, Th36;
then not p . k in {x} by TARSKI:def 1;
then (p - {x}) . (k - 0 ) = p . k by A2, A3, A7, CARD_1:47, FINSEQ_3:92;
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, Th7;
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 set ; :: 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, Th36;
hence y in {(x .. p)} by A11, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: 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, Th29;
then A15: p . (x .. p) in {x} by TARSKI:def 1;
( x .. p in dom p & x .. p <= k + 1 ) by A9, A8, Th30, 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, Th40, FINSEQ_1:def 3;
then k <= (len p) - 1 by A2, FINSEQ_1:3;
then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, XREAL_1:21;
then k + 1 in Seg (len p) ;
then A16: k + 1 in dom p by FINSEQ_1:def 3;

now

x .. p <> k + 1 by A8, XREAL_1:31;
then A17: p . (k + 1) <> x by A1, A16, Th36;
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:92;
then (p - {x}) . ((k + 1) - 1) = p . (k + 1) by A10, CARD_1:50;
hence (p - {x}) . k = p . (k + 1) ; :: thesis: verum