let f be FinSequence; for k being Nat st k <= len f holds
mid (f,k,(len f)) = f /^ (k -' 1)
let k be Nat; ( k <= len f implies mid (f,k,(len f)) = f /^ (k -' 1) )
assume A1:
k <= len f
; 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)
;
hence
mid (f,k,(len f)) = f /^ (k -' 1)
; verum