let p be FinSequence; :: thesis: for x being object holds
( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) )
let x be object ; :: thesis: ( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) )
thus ( p just_once_values x implies ( x in rng p & rng (p |-- x) misses {x} ) ) :: thesis: ( x in rng p & rng (p |-- x) misses {x} implies p just_once_values x )

proof

assume A1: p just_once_values x ; :: thesis: ( x in rng p & rng (p |-- x) misses {x} )
hence x in rng p by Th45; :: thesis: rng (p |-- x) misses {x}
assume not rng (p |-- x) misses {x} ; :: thesis: contradiction
then A2: ex y being object st
( y in rng (p |-- x) & y in {x} ) by XBOOLE_0:3;
not x in rng (p |-- x) by A1, Th45;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

assume that
A3: x in rng p and
A4: rng (p |-- x) misses {x} ; :: thesis: p just_once_values x

now :: thesis: not x in rng (p |-- x)

A5: x in {x} by TARSKI:def 1;
assume x in rng (p |-- x) ; :: thesis: contradiction
hence contradiction by A4, A5, XBOOLE_0:3; :: thesis: verum

end;

hence p just_once_values x by A3, Th45; :: thesis: verum