let D be non empty set ; :: thesis: for f being FinSequence of D st 1 <= len f holds

mid (f,(len f),1) = Rev f

let f be FinSequence of D; :: thesis: ( 1 <= len f implies mid (f,(len f),1) = Rev f )

assume A1: 1 <= len f ; :: thesis: mid (f,(len f),1) = Rev f

A2: 1 -' 1 = 0 by XREAL_1:232;

mid (f,(len f),1) = Rev f

let f be FinSequence of D; :: thesis: ( 1 <= len f implies mid (f,(len f),1) = Rev f )

assume A1: 1 <= len f ; :: thesis: mid (f,(len f),1) = Rev f

A2: 1 -' 1 = 0 by XREAL_1:232;

per cases
( len f <> 1 or len f = 1 )
;

end;

suppose
len f <> 1
; :: thesis: mid (f,(len f),1) = Rev f

then
1 < len f
by A1, XXREAL_0:1;

then mid (f,(len f),1) = Rev ((f /^ (1 -' 1)) | (((len f) -' 1) + 1)) by Def3

.= Rev ((f /^ 0) | (len f)) by A1, A2, XREAL_1:235

.= Rev (f | (len f))

.= Rev f by FINSEQ_1:58 ;

hence mid (f,(len f),1) = Rev f ; :: thesis: verum

end;then mid (f,(len f),1) = Rev ((f /^ (1 -' 1)) | (((len f) -' 1) + 1)) by Def3

.= Rev ((f /^ 0) | (len f)) by A1, A2, XREAL_1:235

.= Rev (f | (len f))

.= Rev f by FINSEQ_1:58 ;

hence mid (f,(len f),1) = Rev f ; :: thesis: verum