let p be FinSequence; :: thesis: for x being set holds
( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) )
let x be set ; :: thesis: ( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) )
thus ( p just_once_values x implies ( x in rng p & not x in rng (p |-- x) ) ) :: thesis: ( x in rng p & not x in rng (p |-- x) implies p just_once_values x )

proof

assume A1: p just_once_values x ; :: thesis: ( x in rng p & not x in rng (p |-- x) )
hence A2: x in rng p by Th7; :: thesis: not x in rng (p |-- x)
assume x in rng (p |-- x) ; :: thesis: contradiction
then consider z being set such that
A3: z in dom (p |-- x) and
A4: (p |-- x) . z = x by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A3;
A5: (p |-- x) . z = p . (z + (x .. p)) by A2, A3, Def7;
z + (x .. p) in dom p by A2, A3, Th58;
then z + (x .. p) = 0 + (x .. p) by A1, A4, A5, Th36;
hence contradiction by A3, FINSEQ_3:26; :: thesis: verum

end;

assume that
A6: x in rng p and
A7: not x in rng (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
A8: k in dom p and
A9: k <> x .. p and
A10: p . k = x ; :: thesis: contradiction

now

per cases ( k < x .. p or x .. p < k ) by A9, XXREAL_0:1;

suppose k < x .. p ; :: thesis: contradiction

then k + 1 <= x .. p by NAT_1:13;
then k <= (x .. p) - 1 by XREAL_1:21;
then ( 1 <= k & k <= len (p -| x) ) by A6, A8, Th46, FINSEQ_3:27;
then A11: k in dom (p -| x) by FINSEQ_3:27;
then x = (p -| x) . k by A6, A10, Th48;
then x in rng (p -| x) by A11, FUNCT_1:def 5;
hence contradiction by A6, Th49; :: thesis: verum

end;

suppose A12: x .. p < k ; :: thesis: contradiction

then consider m being Nat such that
A13: k = (x .. p) + m by NAT_1:10;
(x .. p) + 0 < (x .. p) + m by A12, A13;
then 0 < m by XREAL_1:8;
then A14: 0 + 1 <= m by NAT_1:13;
m + (x .. p) <= len p by A8, A13, FINSEQ_3:27;
then m <= (len p) - (x .. p) by XREAL_1:21;
then m <= len (p |-- x) by A6, Def7;
then A15: m in dom (p |-- x) by A14, FINSEQ_3:27;
then (p |-- x) . m = p . k by A6, A13, Def7;
hence contradiction by A7, A10, A15, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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