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

proof

assume that
A1: p - A = p and
A2: not A misses rng p ; :: thesis: contradiction
len (p - A) <> len p by A2, Th59;
hence contradiction by A1; :: thesis: verum

end;

assume A misses rng p ; :: thesis: p - A = p
then p " A = {} by RELAT_1:138;
then Sgm ((Seg (len p)) \ (p " A)) = idseq (len p) by Th46;
then p * (Sgm ((Seg (len p)) \ (p " A))) = p by FINSEQ_2:54;
hence p - A = p by FINSEQ_1:def 3; :: thesis: verum