let D be non empty set ; :: thesis: for k1, k2 being Nat holds mid ((<*> D),k1,k2) = <*> D
let k1, k2 be Nat; :: thesis: mid ((<*> D),k1,k2) = <*> D

per cases ( k1 <= k2 or k1 > k2 ) ;

suppose k1 <= k2 ; :: thesis: mid ((<*> D),k1,k2) = <*> D

hence mid ((<*> D),k1,k2) = ((<*> D) /^ (k1 -' 1)) | ((k2 -' k1) + 1) by FINSEQ_6:def 3
.= (<*> D) | ((k2 -' k1) + 1) by FINSEQ_6:80
.= <*> D by FINSEQ_5:78 ;
:: thesis: verum

end;

suppose k1 > k2 ; :: thesis: mid ((<*> D),k1,k2) = <*> D

hence mid ((<*> D),k1,k2) = Rev (((<*> D) /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by FINSEQ_6:def 3
.= Rev ((<*> D) | ((k1 -' k2) + 1)) by FINSEQ_6:80
.= Rev (<*> D) by FINSEQ_5:78
.= <*> D by FINSEQ_5:79 ;
:: thesis: verum

end;

end;