let f be FinSequence; :: thesis: for k1, k2 being Nat holds rng (mid (f,k1,k2)) c= rng f

let k1, k2 be Nat; :: thesis: rng (mid (f,k1,k2)) c= rng f

let k1, k2 be Nat; :: thesis: rng (mid (f,k1,k2)) c= rng f

per cases
( k1 <= k2 or k1 > k2 )
;

end;

suppose
k1 <= k2
; :: thesis: rng (mid (f,k1,k2)) c= rng f

then
mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1)
by Def3;

then A1: rng (mid (f,k1,k2)) c= rng (f /^ (k1 -' 1)) by FINSEQ_5:19;

rng (f /^ (k1 -' 1)) c= rng f by FINSEQ_5:33;

hence rng (mid (f,k1,k2)) c= rng f by A1; :: thesis: verum

end;then A1: rng (mid (f,k1,k2)) c= rng (f /^ (k1 -' 1)) by FINSEQ_5:19;

rng (f /^ (k1 -' 1)) c= rng f by FINSEQ_5:33;

hence rng (mid (f,k1,k2)) c= rng f by A1; :: thesis: verum

suppose
k1 > k2
; :: thesis: rng (mid (f,k1,k2)) c= rng f

then
mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))
by Def3;

then rng (mid (f,k1,k2)) = rng ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by FINSEQ_5:57;

then A2: rng (mid (f,k1,k2)) c= rng (f /^ (k2 -' 1)) by FINSEQ_5:19;

rng (f /^ (k2 -' 1)) c= rng f by FINSEQ_5:33;

hence rng (mid (f,k1,k2)) c= rng f by A2; :: thesis: verum

end;then rng (mid (f,k1,k2)) = rng ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by FINSEQ_5:57;

then A2: rng (mid (f,k1,k2)) c= rng (f /^ (k2 -' 1)) by FINSEQ_5:19;

rng (f /^ (k2 -' 1)) c= rng f by FINSEQ_5:33;

hence rng (mid (f,k1,k2)) c= rng f by A2; :: thesis: verum