let p be FinSequence; :: thesis: for x being set holds
( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )
let x be set ; :: 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 Th7; :: thesis: p - {x} = (p -| x) ^ (p |-- x)
then (len (p -| x)) + (len (p |-- x)) = ((x .. p) - 1) + (len (p |-- x)) by Th46
.= ((x .. p) - 1) + ((len p) - (x .. p)) by A2, Def7
.= (len p) - 1
.= len (p - {x}) by A1, Th40 ;
then A3: dom (p - {x}) = Seg ((len (p -| x)) + (len (p |-- x))) by FINSEQ_1:def 3;

A4: now

let k be Nat; :: thesis: ( k in dom (p -| x) implies (p - {x}) . k = (p -| x) . k )
assume A5: k in dom (p -| x) ; :: thesis: (p - {x}) . k = (p -| x) . k
then A6: (p -| x) . k = p . k by A2, Th48;
x .. p <= len p by A2, Th31;
then (x .. p) - 1 <= (len p) - 1 by XREAL_1:11;
then len (p -| x) <= (len p) - 1 by A2, Th46;
then len (p -| x) <= len (p - {x}) by A1, Th40;
then A7: ( Seg (len (p -| x)) c= Seg (len (p - {x})) & Seg (len (p -| x)) = dom (p -| x) & Seg (len (p - {x})) = dom (p - {x}) ) by FINSEQ_1:7, FINSEQ_1:def 3;
k in Seg (len (p -| x)) by A5, FINSEQ_1:def 3;
then k <= len (p -| x) by FINSEQ_1:3;
then k <= (x .. p) - 1 by A2, Th46;
then ( k + 1 <= x .. p & k < k + 1 ) by XREAL_1:21, XREAL_1:31;
then k < x .. p by XXREAL_0:2;
hence (p - {x}) . k = (p -| x) . k by A1, A5, A6, A7, Th41; :: thesis: verum

end;

now

let k be Nat; :: thesis: ( k in dom (p |-- x) implies (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k )
assume A8: k in dom (p |-- x) ; :: thesis: (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k
then A9: (p |-- x) . k = p . (k + (x .. p)) by A2, Def7;
reconsider m = (x .. p) - 1 as Element of NAT by A2, Th32;
set z = k + m;
A10: dom (p |-- x) = Seg (len (p |-- x)) by FINSEQ_1:def 3;
then A11: ( 1 <= k & 1 <= x .. p ) by A2, A8, Th31, FINSEQ_1:3;
then 1 + 1 <= k + (x .. p) by XREAL_1:9;
then A12: 1 <= (k + (x .. p)) - 1 by XREAL_1:21;
k <= len (p |-- x) by A8, A10, FINSEQ_1:3;
then k <= (len p) - (x .. p) by A2, Def7;
then k + (x .. p) <= len p by XREAL_1:21;
then (k + (x .. p)) - 1 <= (len p) - 1 by XREAL_1:11;
then ( (k + (x .. p)) - 1 <= len (p - {x}) & dom (p - {x}) = Seg (len (p - {x})) ) by A1, Th40, FINSEQ_1:def 3;
then A13: k + m in dom (p - {x}) by A12;
(x .. p) + 1 <= k + (x .. p) by A11, XREAL_1:9;
then x .. p <= (k + (x .. p)) - 1 by XREAL_1:21;
then (p - {x}) . (k + m) = p . ((k + m) + 1) by A1, A13, Th41
.= p . (k + (x .. p)) ;
hence (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k by A2, A9, Th46; :: thesis: verum

end;

hence p - {x} = (p -| x) ^ (p |-- x) by A3, A4, FINSEQ_1:def 7; :: thesis: verum

end;

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

now

let k be Nat; :: thesis: ( k in dom p & k <> x .. p implies not p . k = x )
assume that
A16: k in dom p and
A17: k <> x .. p and
A18: p . k = x ; :: thesis: contradiction
A19: len (p - {x}) = (len p) - (card (p " {x})) by FINSEQ_3:66
.= (len p) + (- (card (p " {x}))) ;
A20: len (p - {x}) = (len (p -| x)) + (len (p |-- x)) by A15, FINSEQ_1:35
.= ((x .. p) - 1) + (len (p |-- x)) by A14, Th46
.= ((x .. p) - 1) + ((len p) - (x .. p)) by A14, Def7
.= (len p) + (- 1) ;
{(x .. p),k} c= p " {x}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {(x .. p),k} or y in p " {x} )
assume A21: y in {(x .. p),k} ; :: thesis: y in p " {x}
( x in {x} & x .. p in dom p & p . (x .. p) = x ) by A14, Th29, Th30, TARSKI:def 1;
then ( x .. p in p " {x} & k in p " {x} ) by A16, A18, FUNCT_1:def 13;
hence y in p " {x} by A21, TARSKI:def 2; :: thesis: verum

end;

then card {(x .. p),k} <= card (p " {x}) by NAT_1:44;
then 2 <= card (p " {x}) by A17, CARD_2:76;
hence contradiction by A19, A20; :: thesis: verum

end;

hence p just_once_values x by A14, Th37; :: thesis: verum