let k be Nat; for f1 being FinSequence st len f1 < k holds
mid (f1,k,k) = {}
let f1 be FinSequence; ( len f1 < k implies mid (f1,k,k) = {} )
assume A1:
len f1 < k
; 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 FINSEQ_6:def 3;
hence
mid (f1,k,k) = {}
by A3; verum