let p be FinSequence; :: thesis: for x being object st x in rng p holds
rng (p -| x) misses {x}
let x be object ; :: thesis: ( x in rng p implies rng (p -| x) misses {x} )
assume x in rng p ; :: thesis: rng (p -| x) misses {x}
then not x in rng (p -| x) by Th37;
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