let p be FinSequence; for A being set holds rng (p - A) = (rng p) \ A
let A be set ; 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;
A2:
dom p = Seg (len p)
by FINSEQ_1:def 3;
thus
rng (p - A) c= (rng p) \ A
XBOOLE_0:def 10 (rng p) \ A c= rng (p - A)proof
let x be
object ;
TARSKI:def 3 ( 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)
;
x in (rng p) \ A
A5:
now not x in AA6:
(Seg (len p)) \ (p " A) c= Seg (len p)
by XBOOLE_1:36;
assume A7:
x in A
;
contradictionconsider 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 A2, A8, FUNCT_1:11;
then A11:
(p - A) . y = p . ((Sgm ((Seg (len p)) \ (p " A))) . y)
by A2, 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 A6, FINSEQ_1:def 13;
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 A2, A8, FUNCT_1:11;
hence
contradiction
by A7, A9, A11, A12, FUNCT_1:def 7;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in (rng p) \ A or x in rng (p - A) )
assume A13:
x in (rng p) \ A
; 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;
(Seg (len p)) \ (p " A) c= Seg (len p)
by XBOOLE_1:36;
then A16:
rng (Sgm ((Seg (len p)) \ (p " A))) = (Seg (len p)) \ (p " A)
by FINSEQ_1:def 13;
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 A2, A15, A17, A18, FUNCT_1:13;
z in dom (p - A)
by A2, A14, A17, A18, FUNCT_1:11;
hence
x in rng (p - A)
by A19, FUNCT_1:def 3; verum