let D be set ; for p being FinSequence of D
for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p
let p be FinSequence of D; for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p
let i, j be Element of NAT ; rng (Del (p,i,j)) c= rng p
A1:
rng (p /^ j) c= rng p
rng (p | (i -' 1)) = rng (p | (Seg (i -' 1)))
by FINSEQ_1:def 15;
then A4:
rng (p | (i -' 1)) c= rng p
by RELAT_1:70;
rng ((p | (i -' 1)) ^ (p /^ j)) = (rng (p | (i -' 1))) \/ (rng (p /^ j))
by FINSEQ_1:31;
hence
rng (Del (p,i,j)) c= rng p
by A4, A1, XBOOLE_1:8; verum