let p be FinSequence; :: thesis: for x being object st x in rng p & p is one-to-one holds
rng (p |-- x) misses {x}
let x be object ; :: thesis: ( x in rng p & p is one-to-one implies rng (p |-- x) misses {x} )
assume ( x in rng p & p is one-to-one ) ; :: thesis: rng (p |-- x) misses {x}
then not x in rng (p |-- x) by Th46;
then for y being object st y in rng (p |-- x) holds
not y in {x} by TARSKI:def 1;
hence rng (p |-- x) misses {x} by XBOOLE_0:3; :: thesis: verum