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;

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

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;

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

then A4: f | 1 = f by FINSEQ_1:58;
mid (f,(len f),1) = (f /^ (1 -' 1)) | ((1 -' 1) + 1) by A3, Def3
.= f | 1 by A2 ;
hence mid (f,(len f),1) = Rev f by A1, A4, Th110, FINSEQ_1:59; :: thesis: verum

end;

end;