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

proof

assume that
A1: p - A = {} and
A2: not rng p c= A ; :: thesis: contradiction
(rng p) \ A <> {} by A2, XBOOLE_1:37;
then rng (p - A) <> {} by Th63;
hence contradiction by A1; :: thesis: verum

end;

assume A3: rng p c= A ; :: thesis: p - A = {}
rng (p - A) = (rng p) \ A by Th63;
hence p - A = {} by A3, XBOOLE_1:37; :: thesis: verum