let D be non empty set ; :: thesis: for f1 being FinSequence of D
for k being Element of NAT st len f1 < k holds
mid f1,k,k = <*> D
let f1 be FinSequence of D; :: thesis: for k being Element of NAT st len f1 < k holds
mid f1,k,k = <*> D
let k be Element of NAT ; :: thesis: ( len f1 < k implies mid f1,k,k = <*> D )
assume A1: len f1 < k ; :: thesis: mid f1,k,k = <*> D
then A2: 0 + 1 <= k by NAT_1:13;
(k -' k) + 1 = (k - k) + 1 by XREAL_1:235
.= 1 ;
then A3: mid f1,k,k = (f1 /^ (k -' 1)) | 1 by JORDAN3:def 1;
(len f1) + 1 <= k by A1, NAT_1:13;
then ((len f1) + 1) - 1 <= k - 1 by XREAL_1:11;
then len f1 <= k -' 1 by A2, XREAL_1:235;
then f1 /^ (k -' 1) = <*> D by FINSEQ_5:35;
hence mid f1,k,k = <*> D by A3, FINSEQ_5:81; :: thesis: verum