let p be FinSequence; :: thesis: for x being set holds
( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) )
let x be set ; :: 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 Th60; :: thesis: rng (p |-- x) misses {x}
A2: not x in rng (p |-- x) by A1, Th60;
assume not rng (p |-- x) misses {x} ; :: thesis: contradiction
then ex y being set st
( y in rng (p |-- x) & y in {x} ) by XBOOLE_0:3;
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

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

end;

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