let p be FinSequence; :: thesis: for x being set holds
( p - {x} = p iff not x in rng p )
let x be set ; :: thesis: ( p - {x} = p iff not x in rng p )
thus ( p - {x} = p implies not x in rng p ) :: thesis: ( not x in rng p implies p - {x} = p )

proof

assume p - {x} = p ; :: thesis: not x in rng p
then A1: {x} misses rng p by Th76;
x in {x} by TARSKI:def 1;
hence not x in rng p by A1, XBOOLE_0:3; :: thesis: verum

end;

assume A2: not x in rng p ; :: thesis: p - {x} = p
{x} misses rng p

proof

assume {x} meets rng p ; :: thesis: contradiction
then ex y being set st
( y in {x} & y in rng p ) by XBOOLE_0:3;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

hence p - {x} = p by Th76; :: thesis: verum