let p be FinSequence; :: thesis: for A being set holds rng (p - A) = (rng p) \ A
let A be set ; :: thesis: rng (p - A) = (rng p) \ A
set q = Sgm ((Seg (len p)) \ (p " A));
A1: dom p = Seg (len p) by FINSEQ_1:def 3;
thus rng (p - A) c= (rng p) \ A :: according to XBOOLE_0:def 10 :: thesis: (rng p) \ A c= rng (p - A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (p - A) or x in (rng p) \ A )
A3: rng (p * (Sgm ((Seg (len p)) \ (p " A)))) c= rng p by RELAT_1:26;
assume A4: x in rng (p - A) ; :: thesis: x in (rng p) \ A

A5: now :: thesis: not x in A

assume A7: x in A ; :: thesis: contradiction
consider y being object such that
A8: y in dom (p - A) and
A9: (p - A) . y = x by A4, FUNCT_1:def 3;
set z = (Sgm ((Seg (len p)) \ (p " A))) . y;
A10: y in dom (Sgm ((Seg (len p)) \ (p " A))) by A1, A8, FUNCT_1:11;
then A11: (p - A) . y = p . ((Sgm ((Seg (len p)) \ (p " A))) . y) by A1, FUNCT_1:13;
(Sgm ((Seg (len p)) \ (p " A))) . y in rng (Sgm ((Seg (len p)) \ (p " A))) by A10, FUNCT_1:def 3;
then (Sgm ((Seg (len p)) \ (p " A))) . y in (Seg (len p)) \ (p " A) by FINSEQ_1:def 14;
then A12: not (Sgm ((Seg (len p)) \ (p " A))) . y in p " A by XBOOLE_0:def 5;
(Sgm ((Seg (len p)) \ (p " A))) . y in dom p by A1, A8, FUNCT_1:11;
hence contradiction by A7, A9, A11, A12, FUNCT_1:def 7; :: thesis: verum

end;

x in rng (p * (Sgm ((Seg (len p)) \ (p " A)))) by A4, FINSEQ_1:def 3;
hence x in (rng p) \ A by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng p) \ A or x in rng (p - A) )
assume A13: x in (rng p) \ A ; :: thesis: x in rng (p - A)
then consider y being object such that
A14: y in dom p and
A15: p . y = x by FUNCT_1:def 3;
A16: rng (Sgm ((Seg (len p)) \ (p " A))) = (Seg (len p)) \ (p " A) by FINSEQ_1:def 14;
not p . y in A by A13, A15, XBOOLE_0:def 5;
then not y in p " A by FUNCT_1:def 7;
then y in rng (Sgm ((Seg (len p)) \ (p " A))) by A14, A1, A16, XBOOLE_0:def 5;
then consider z being object such that
A17: z in dom (Sgm ((Seg (len p)) \ (p " A))) and
A18: (Sgm ((Seg (len p)) \ (p " A))) . z = y by FUNCT_1:def 3;
A19: (p - A) . z = x by A1, A15, A17, A18, FUNCT_1:13;
z in dom (p - A) by A1, A14, A17, A18, FUNCT_1:11;
hence x in rng (p - A) by A19, FUNCT_1:def 3; :: thesis: verum