let f be FinSequence; :: thesis: ( 1 <= len f implies mid (f,1,(len f)) = f )
assume A1: 1 <= len f ; :: thesis: mid (f,1,(len f)) = f
then mid (f,1,(len f)) = (f /^ (1 -' 1)) | (((len f) -' 1) + 1) by Def3
.= (f /^ 0) | (((len f) -' 1) + 1) by XREAL_1:232
.= f | (((len f) -' 1) + 1)
.= f | (len f) by A1, XREAL_1:235
.= f by FINSEQ_1:58 ;
hence mid (f,1,(len f)) = f ; :: thesis: verum