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
rng (p | (i -' 1)) = rng (p | (Seg (i -' 1))) by FINSEQ_1:def 15;
then A1: rng (p | (i -' 1)) c= rng p by RELAT_1:99;
A2: rng (p /^ j) c= rng p

proof

per cases ( D is empty or not D is empty ) ;

suppose D is empty ; :: thesis: rng (p /^ j) c= rng p

then A3: rng p = {} ;
then A4: p = {} ;

A5: now

assume j <= len p ; :: thesis: rng (p /^ j) c= rng p
then j <= 0 by A4;
then j = 0 ;
then len (p /^ j) = (len p) - 0 by RFINSEQ:def 2;
then len (p /^ j) = 0 - 0 by A4;
then p /^ j = {} ;
hence rng (p /^ j) c= rng p by A4; :: thesis: verum

end;

now

assume j > len p ; :: thesis: rng (p /^ j) c= rng p
then p /^ j = <*> D by RFINSEQ:def 2;
hence rng (p /^ j) c= rng p by A3; :: thesis: verum

end;

hence rng (p /^ j) c= rng p by A5; :: thesis: verum

end;

suppose not D is empty ; :: thesis: rng (p /^ j) c= rng p

then reconsider E = D as non empty set ;
reconsider r = p as FinSequence of E ;
rng (r /^ j) c= rng r by FINSEQ_5:36;
hence rng (p /^ j) c= rng p ; :: thesis: verum

end;

end;

end;

rng ((p | (i -' 1)) ^ (p /^ j)) = (rng (p | (i -' 1))) \/ (rng (p /^ j)) by FINSEQ_1:44;
hence rng (Del p,i,j) c= rng p by A1, A2, XBOOLE_1:8; :: thesis: verum