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:234;

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

end;

end;