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 Def1
.= (f /^ 0 ) | (((len f) -' 1) + 1) by XREAL_1:234
.= f | (((len f) -' 1) + 1) by FINSEQ_5:31
.= f | (len f) by A1, XREAL_1:237
.= f by FINSEQ_1:79 ;
hence mid f,1,(len f) = f ; :: thesis: verum