let f be FinSequence; :: thesis: for k being Nat st k <= len f holds
mid (f,k,(len f)) = f /^ (k -' 1)
let k be 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 Def3;
k -' 1 <= len f by A1, NAT_D:44;
then A3: len (f /^ (k -' 1)) = (len f) - (k -' 1) by RFINSEQ:def 1;
A4: ((len f) -' k) + 1 = ((len f) - k) + 1 by A1, XREAL_1:233
.= (len f) - (k - 1) ;

now :: thesis: ( ( k = 0 & mid (f,k,(len f)) = f /^ (k -' 1) ) or ( k <> 0 & mid (f,k,(len f)) = f /^ (k -' 1) ) )

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

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

0 - 1 < 0 ;
then k -' 1 = 0 by A5, XREAL_0:def 2;
then A6: f /^ (k -' 1) = f ;
((len f) -' k) + 1 = (len f) + 1 by A5, NAT_D:40;
then len f <= ((len f) -' k) + 1 by NAT_1:11;
then Seg (len f) c= Seg (((len f) -' k) + 1) by FINSEQ_1:5;
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:68;
hence mid (f,k,(len f)) = f /^ (k -' 1) by A2; :: thesis: verum

end;

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

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

end;

end;

end;

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