let D be non empty set ; :: thesis: for k1, k2 being Element of NAT holds mid (<*> D),k1,k2 = <*> D
let k1, k2 be Element of 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:86
.= <*> D by FINSEQ_5:81 ;
:: 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:86
.= Rev (<*> D) by FINSEQ_5:81
.= <*> D by FINSEQ_5:82 ;
:: thesis: verum

end;

end;