let f1 be FinSequence; :: thesis: mid (f1,0,0) = f1 | 1
0 - 1 < 0 ;
then A1: 0 -' 1 = 0 by XREAL_0:def 2;
(0 -' 0) + 1 = (0 - 0) + 1 by XREAL_1:233
.= 1 ;
then mid (f1,0,0) = (f1 /^ (0 -' 1)) | 1 by FINSEQ_6:def 3;
hence mid (f1,0,0) = f1 | 1 by A1; :: thesis: verum