let k be Nat; :: thesis: for f1 being FinSequence st len f1 < k holds
mid (f1,k,k) = {}
let f1 be FinSequence; :: thesis: ( len f1 < k implies mid (f1,k,k) = {} )
assume A1: len f1 < k ; :: thesis: mid (f1,k,k) = {}
then (len f1) + 1 <= k by NAT_1:13;
then A2: ((len f1) + 1) - 1 <= k - 1 by XREAL_1:9;
0 + 1 <= k by A1, NAT_1:13;
then len f1 <= k -' 1 by A2, XREAL_1:233;
then A3: f1 /^ (k -' 1) = {} by FINSEQ_5:32;
(k -' k) + 1 = (k - k) + 1 by XREAL_1:233
.= 1 ;
then mid (f1,k,k) = (f1 /^ (k -' 1)) | 1 by Def3;
hence mid (f1,k,k) = {} by A3; :: thesis: verum