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
proof
per cases ( D is empty or not D is empty ) ;
suppose A2: D is empty ; :: thesis: rng (p /^ j) c= rng p
then A3: ( j > len p implies rng (p /^ j) c= rng p ) ;
( j <= len p implies rng (p /^ j) c= rng p ) by A2;
hence rng (p /^ j) c= rng p by A3; :: 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:33;
hence rng (p /^ j) c= rng p ; :: thesis: verum
end;
end;
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