let p be FinSequence; :: thesis: for x being object holds
( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )
let x be object ; :: thesis: ( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )
set q = p - {x};
set r = p -| x;
set s = p |-- x;
thus ( p just_once_values x implies ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) ) :: thesis: ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) implies p just_once_values x )

proof

assume A1: p just_once_values x ; :: thesis: ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) )
hence A2: x in rng p by Th5; :: thesis: p - {x} = (p -| x) ^ (p |-- x)

A3: now :: thesis: for k being Nat st k in dom (p -| x) holds
(p - {x}) . k = (p -| x) . k

x .. p <= len p by A2, Th21;
then (x .. p) - 1 <= (len p) - 1 by XREAL_1:9;
then len (p -| x) <= (len p) - 1 by A2, Th34;
then len (p -| x) <= len (p - {x}) by A1, Th30;
then A4: Seg (len (p -| x)) c= Seg (len (p - {x})) by FINSEQ_1:5;
let k be Nat; :: thesis: ( k in dom (p -| x) implies (p - {x}) . k = (p -| x) . k )
A5: ( Seg (len (p -| x)) = dom (p -| x) & Seg (len (p - {x})) = dom (p - {x}) ) by FINSEQ_1:def 3;
assume A6: k in dom (p -| x) ; :: thesis: (p - {x}) . k = (p -| x) . k
then k in Seg (len (p -| x)) by FINSEQ_1:def 3;
then k <= len (p -| x) by FINSEQ_1:1;
then k <= (x .. p) - 1 by A2, Th34;
then A7: k + 1 <= x .. p by XREAL_1:19;
k < k + 1 by XREAL_1:29;
then A8: k < x .. p by A7, XXREAL_0:2;
(p -| x) . k = p . k by A2, A6, Th36;
hence (p - {x}) . k = (p -| x) . k by A1, A6, A4, A5, A8, Th31; :: thesis: verum

end;

A9: now :: thesis: for k being Nat st k in dom (p |-- x) holds
(p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k

reconsider m = (x .. p) - 1 as Element of NAT by A2, Th22;
let k be Nat; :: thesis: ( k in dom (p |-- x) implies (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k )
set z = k + m;
assume A10: k in dom (p |-- x) ; :: thesis: (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k
then A11: (p |-- x) . k = p . (k + (x .. p)) by A2, Def6;
A12: dom (p |-- x) = Seg (len (p |-- x)) by FINSEQ_1:def 3;
then A13: 1 <= k by A10, FINSEQ_1:1;
then (x .. p) + 1 <= k + (x .. p) by XREAL_1:7;
then A14: x .. p <= (k + (x .. p)) - 1 by XREAL_1:19;
k <= len (p |-- x) by A10, A12, FINSEQ_1:1;
then k <= (len p) - (x .. p) by A2, Def6;
then k + (x .. p) <= len p by XREAL_1:19;
then (k + (x .. p)) - 1 <= (len p) - 1 by XREAL_1:9;
then A15: (k + (x .. p)) - 1 <= len (p - {x}) by A1, Th30;
1 <= x .. p by A2, Th21;
then 1 + 1 <= k + (x .. p) by A13, XREAL_1:7;
then A16: 1 <= (k + (x .. p)) - 1 by XREAL_1:19;
dom (p - {x}) = Seg (len (p - {x})) by FINSEQ_1:def 3;
then k + m in dom (p - {x}) by A16, A15;
then (p - {x}) . (k + m) = p . ((k + m) + 1) by A1, A14, Th31
.= p . (k + (x .. p)) ;
hence (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k by A2, A11, Th34; :: thesis: verum

end;

(len (p -| x)) + (len (p |-- x)) = ((x .. p) - 1) + (len (p |-- x)) by A2, Th34
.= ((x .. p) - 1) + ((len p) - (x .. p)) by A2, Def6
.= (len p) - 1
.= len (p - {x}) by A1, Th30 ;
then dom (p - {x}) = Seg ((len (p -| x)) + (len (p |-- x))) by FINSEQ_1:def 3;
hence p - {x} = (p -| x) ^ (p |-- x) by A3, A9, FINSEQ_1:def 7; :: thesis: verum

end;

assume A17: x in rng p ; :: thesis: ( not p - {x} = (p -| x) ^ (p |-- x) or p just_once_values x )
assume A18: p - {x} = (p -| x) ^ (p |-- x) ; :: thesis: p just_once_values x

now :: thesis: for k being Nat st k in dom p & k <> x .. p holds
not p . k = x

let k be Nat; :: thesis: ( k in dom p & k <> x .. p implies not p . k = x )
assume that
A19: k in dom p and
A20: k <> x .. p and
A21: p . k = x ; :: thesis: contradiction
{(x .. p),k} c= p " {x}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {(x .. p),k} or y in p " {x} )
assume A22: y in {(x .. p),k} ; :: thesis: y in p " {x}
A23: x in {x} by TARSKI:def 1;
( x .. p in dom p & p . (x .. p) = x ) by A17, Th19, Th20;
then A24: x .. p in p " {x} by A23, FUNCT_1:def 7;
k in p " {x} by A19, A21, A23, FUNCT_1:def 7;
hence y in p " {x} by A22, A24, TARSKI:def 2; :: thesis: verum

end;

then card {(x .. p),k} <= card (p " {x}) by NAT_1:43;
then A25: 2 <= card (p " {x}) by A20, CARD_2:57;
A26: len (p - {x}) = (len p) - (card (p " {x})) by FINSEQ_3:59
.= (len p) + (- (card (p " {x}))) ;
len (p - {x}) = (len (p -| x)) + (len (p |-- x)) by A18, FINSEQ_1:22
.= ((x .. p) - 1) + (len (p |-- x)) by A17, Th34
.= ((x .. p) - 1) + ((len p) - (x .. p)) by A17, Def6
.= (len p) + (- 1) ;
hence contradiction by A26, A25; :: thesis: verum

end;

hence p just_once_values x by A17, Th27; :: thesis: verum