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

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