let p be FinSequence; :: thesis: for x being object holds
( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) )
let x be object ; :: 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 Th5; :: thesis: not x in rng (p |-- x)
assume x in rng (p |-- x) ; :: thesis: contradiction
then consider z being object such that
A3: z in dom (p |-- x) and
A4: (p |-- x) . z = x by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A3;
( (p |-- x) . z = p . (z + (x .. p)) & z + (x .. p) in dom p ) by A2, A3, Def6, Th43;
then z + (x .. p) = 0 + (x .. p) by A1, A4, Th26;
hence contradiction by A3, FINSEQ_3:24; :: thesis: verum

end;

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

now :: thesis: contradiction

per cases ( k < x .. p or x .. p < k ) by A8, 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:19;
then A10: k <= len (p -| x) by A5, Th34;
1 <= k by A7, FINSEQ_3:25;
then A11: k in dom (p -| x) by A10, FINSEQ_3:25;
then x = (p -| x) . k by A5, A9, Th36;
then x in rng (p -| x) by A11, FUNCT_1:def 3;
hence contradiction by A5, Th37; :: 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 ;
then A14: 0 + 1 <= m by NAT_1:13;
m + (x .. p) <= len p by A7, A13, FINSEQ_3:25;
then m <= (len p) - (x .. p) by XREAL_1:19;
then m <= len (p |-- x) by A5, Def6;
then A15: m in dom (p |-- x) by A14, FINSEQ_3:25;
then (p |-- x) . m = p . k by A5, A13, Def6;
hence contradiction by A6, A9, A15, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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