let D be non empty set ; :: thesis: for f1 being FinSequence of D
for k being Nat st len f1 < k holds
mid (f1,k,k) = <*> D
let f1 be FinSequence of D; :: thesis: for k being Nat st len f1 < k holds
mid (f1,k,k) = <*> D
let k be Nat; :: thesis: ( len f1 < k implies mid (f1,k,k) = <*> D )
assume A1: len f1 < k ; :: thesis: mid (f1,k,k) = <*> D
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) = <*> D 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) = <*> D by A3, Lm2; :: thesis: verum