let D be non empty set ; :: thesis: for f1 being FinSequence of D holds mid f1,0 ,0 = f1 | 1
let f1 be FinSequence of D; :: thesis: mid f1,0 ,0 = f1 | 1
(0 -' 0 ) + 1 = (0 - 0 ) + 1 by XREAL_1:235
.= 1 ;
then A1: mid f1,0 ,0 = (f1 /^ (0 -' 1)) | 1 by JORDAN3:def 1;
0 - 1 < 0 ;
then 0 -' 1 = 0 by XREAL_0:def 2;
hence mid f1,0 ,0 = f1 | 1 by A1, FINSEQ_5:31; :: thesis: verum