let D be non empty set ; :: thesis: for f being FinSequence of D
for k being Element of NAT st k <= len f holds
mid f,k,(len f) = f /^ (k -' 1)
let f be FinSequence of D; :: thesis: for k being Element of NAT st k <= len f holds
mid f,k,(len f) = f /^ (k -' 1)
let k be Element of NAT ; :: thesis: ( k <= len f implies mid f,k,(len f) = f /^ (k -' 1) )
assume A1: k <= len f ; :: thesis: mid f,k,(len f) = f /^ (k -' 1)
then A2: mid f,k,(len f) = (f /^ (k -' 1)) | (((len f) -' k) + 1) by Def1;
k -' 1 <= len f by A1, NAT_D:44;
then A3: len (f /^ (k -' 1)) = (len f) - (k -' 1) by RFINSEQ:def 2;
A4: ((len f) -' k) + 1 = ((len f) - k) + 1 by A1, XREAL_1:235
.= (len f) - (k - 1) ;

now

per cases ( k = 0 or k <> 0 ) ;

case A5: k = 0 ; :: thesis: mid f,k,(len f) = f /^ (k -' 1)

then ((len f) -' k) + 1 = (len f) + 1 by NAT_D:40;
then len f <= ((len f) -' k) + 1 by NAT_1:11;
then A6: Seg (len f) c= Seg (((len f) -' k) + 1) by FINSEQ_1:7;
0 - 1 < 0 ;
then k -' 1 = 0 by A5, XREAL_0:def 2;
then f /^ (k -' 1) = f by FINSEQ_5:31;
then dom (f /^ (k -' 1)) c= Seg (((len f) -' k) + 1) by A6, FINSEQ_1:def 3;
then (f /^ (k -' 1)) | (Seg (((len f) -' k) + 1)) = f /^ (k -' 1) by RELAT_1:97;
hence mid f,k,(len f) = f /^ (k -' 1) by A2, FINSEQ_1:def 15; :: thesis: verum

end;

case k <> 0 ; :: thesis: mid f,k,(len f) = f /^ (k -' 1)

then k > 0 ;
then 0 + 1 <= k by NAT_1:13;
then len (f /^ (k -' 1)) = ((len f) -' k) + 1 by A3, A4, XREAL_1:235;
hence mid f,k,(len f) = (f /^ (k -' 1)) | (Seg (len (f /^ (k -' 1)))) by A2, FINSEQ_1:def 15
.= (f /^ (k -' 1)) | (dom (f /^ (k -' 1))) by FINSEQ_1:def 3
.= f /^ (k -' 1) by RELAT_1:97 ;
:: thesis: verum

end;

end;

end;

hence mid f,k,(len f) = f /^ (k -' 1) ; :: thesis: verum