let D be non empty set ; :: thesis: for f being FinSequence of D st 1 <= len f holds
mid (f,1,(len f)) = f
let f be FinSequence of D; :: 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) by FINSEQ_5:28
.= f | (len f) by A1, XREAL_1:235
.= f by FINSEQ_1:58 ;
hence mid (f,1,(len f)) = f ; :: thesis: verum