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) ) )
then A2: x in rng p by Th7;
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 A3: 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) ) )
A4: dom (p - {x}) c= dom p by FINSEQ_3:70;
set A = { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } ;
set q = p - {x};
set B = { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } ;
thus ( k < x .. p implies (p - {x}) . k = p . k ) :: thesis: ( x .. p <= k implies (p - {x}) . k = p . (k + 1) )

proof

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

proof

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

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
A7: L in dom p and
A8: L <= k and
A9: p . L in {x} ;
( p . L <> x & p . L = x ) by A1, A5, A7, A8, A9, Th36, TARSKI:def 1;
hence y in {} ; :: thesis: verum

end;

thus {} c= { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } by XBOOLE_1:2; :: thesis: verum

end;

p . k <> x by A1, A3, A4, A5, Th36;
then not p . k in {x} by TARSKI:def 1;
then (p - {x}) . (k - 0 ) = p . k by A3, A4, A6, CARD_1:47, FINSEQ_3:92;
hence (p - {x}) . k = p . k ; :: thesis: verum

end;

assume A10: x .. p <= k ; :: thesis: (p - {x}) . k = p . (k + 1)
A11: { 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
A12: M = y and
A13: M in dom p and
M <= k + 1 and
A14: p . M in {x} ;
p . M = x by A14, TARSKI:def 1;
then M = x .. p by A1, A13, Th36;
hence y in {(x .. p)} by A12, 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 A15: y = x .. p by TARSKI:def 1;
A16: x .. p in dom p by A2, Th30;
A17: x .. p <= k + 1 by A10, NAT_1:12;
p . (x .. p) = x by A2, Th29;
then p . (x .. p) in {x} by TARSKI:def 1;
hence y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } by A15, A16, A17; :: 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 ( 1 <= k & k <= (len p) - 1 & k <= k + 1 ) by A3, 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 A18: k + 1 in dom p by FINSEQ_1:def 3;

now

assume A19: p . (k + 1) in {x} ; :: thesis: contradiction
x .. p <> k + 1 by A10, XREAL_1:31;
then p . (k + 1) <> x by A1, A18, Th36;
hence contradiction by A19, TARSKI:def 1; :: thesis: verum

end;

then (p - {x}) . ((k + 1) - (card B)) = p . (k + 1) by A18, FINSEQ_3:92;
then (p - {x}) . ((k + 1) - 1) = p . (k + 1) by A11, CARD_1:50;
hence (p - {x}) . k = p . (k + 1) ; :: thesis: verum