let p be FinSequence; :: thesis: for x being set holds
( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )
let x be set ; :: 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 Th35;
hence ( x in rng p & {(x .. p)} = p " {x} ) by A1, Th7, Th17; :: thesis: verum

end;

assume that
A2: x in rng p and
A3: {(x .. p)} = p " {x} ; :: thesis: p just_once_values x
A4: ( p . (x .. p) = x & x .. p in dom p ) by A2, Th29, Th30;

now

let z be set ; :: 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 13;
hence contradiction by A3, A6, TARSKI:def 1; :: thesis: verum

end;

hence p just_once_values x by A4, Th9; :: thesis: verum