let p be FinSequence; :: thesis: for x being object holds
( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )
let x be object ; :: thesis: ( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )
thus ( p just_once_values x implies ( x in rng p & {(x .. p)} = p " {x} ) ) :: thesis: ( x in rng p & {(x .. p)} = p " {x} implies p just_once_values x )

proof

assume A1: p just_once_values x ; :: thesis: ( x in rng p & {(x .. p)} = p " {x} )
then x .. p = p <- x by Th25;
hence ( x in rng p & {(x .. p)} = p " {x} ) by A1, Th5, Th11; :: thesis: verum

end;

assume that
A2: x in rng p and
A3: {(x .. p)} = p " {x} ; :: thesis: p just_once_values x

A4: now :: thesis: for z being object st z in dom p & z <> x .. p holds
not p . z = x

let z be object ; :: thesis: ( z in dom p & z <> x .. p implies not p . z = x )
assume that
A5: z in dom p and
A6: z <> x .. p and
A7: p . z = x ; :: thesis: contradiction
p . z in {x} by A7, TARSKI:def 1;
then z in p " {x} by A5, FUNCT_1:def 7;
hence contradiction by A3, A6, TARSKI:def 1; :: thesis: verum

end;

( p . (x .. p) = x & x .. p in dom p ) by A2, Th19, Th20;
hence p just_once_values x by A4, Th7; :: thesis: verum