let D be set ; :: thesis: 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; :: thesis: for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p

let i, j be Element of NAT ; :: thesis: rng (Del (p,i,j)) c= rng p

A1: rng (p /^ j) c= rng p

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; :: thesis: verum

for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p

let p be FinSequence of D; :: thesis: for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p

let i, j be Element of NAT ; :: thesis: rng (Del (p,i,j)) c= rng p

A1: rng (p /^ j) c= rng p

proof
end;

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; :: thesis: verum