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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (p - A) or x in (rng p) \ A )
assume A2: x in rng (p - A) ; :: thesis: x in (rng p) \ A
then A3: ( x in rng (p * (Sgm ((Seg (len p)) \ (p " A)))) & rng (p * (Sgm ((Seg (len p)) \ (p " A)))) c= rng p ) by FINSEQ_1:def 3, RELAT_1:45;

now

assume A4: x in A ; :: thesis: contradiction
consider y being set such that
A5: y in dom (p - A) and
A6: (p - A) . y = x by A2, FUNCT_1:def 5;
set z = (Sgm ((Seg (len p)) \ (p " A))) . y;
A7: y in dom (Sgm ((Seg (len p)) \ (p " A))) by A1, A5, FUNCT_1:21;
then A8: (Sgm ((Seg (len p)) \ (p " A))) . y in rng (Sgm ((Seg (len p)) \ (p " A))) by FUNCT_1:def 5;
A9: (Sgm ((Seg (len p)) \ (p " A))) . y in dom p by A1, A5, FUNCT_1:21;
A10: (p - A) . y = p . ((Sgm ((Seg (len p)) \ (p " A))) . y) by A1, A7, FUNCT_1:23;
(Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then (Sgm ((Seg (len p)) \ (p " A))) . y in (Seg (len p)) \ (p " A) by A8, FINSEQ_1:def 13;
then not (Sgm ((Seg (len p)) \ (p " A))) . y in p " A by XBOOLE_0:def 5;
hence contradiction by A4, A6, A9, A10, FUNCT_1:def 13; :: thesis: verum

end;

hence x in (rng p) \ A by A3, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng p) \ A or x in rng (p - A) )
assume A11: x in (rng p) \ A ; :: thesis: x in rng (p - A)
then consider y being set such that
A12: y in dom p and
A13: p . y = x by FUNCT_1:def 5;
not p . y in A by A11, A13, XBOOLE_0:def 5;
then A14: not y in p " A by FUNCT_1:def 13;
(Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then ( dom p = Seg (len p) & rng (Sgm ((Seg (len p)) \ (p " A))) = (Seg (len p)) \ (p " A) ) by FINSEQ_1:def 3, FINSEQ_1:def 13;
then y in rng (Sgm ((Seg (len p)) \ (p " A))) by A12, A14, XBOOLE_0:def 5;
then consider z being set such that
A15: z in dom (Sgm ((Seg (len p)) \ (p " A))) and
A16: (Sgm ((Seg (len p)) \ (p " A))) . z = y by FUNCT_1:def 5;
A17: z in dom (p - A) by A1, A12, A15, A16, FUNCT_1:21;
(p - A) . z = x by A1, A13, A15, A16, FUNCT_1:23;
hence x in rng (p - A) by A17, FUNCT_1:def 5; :: thesis: verum