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

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

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;

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;

end;