let f be FinSequence; for k being Nat st 1 <= k holds
mid (f,1,k) = f | k
let k be Nat; ( 1 <= k implies mid (f,1,k) = f | k )
1 -' 1 = 0
by XREAL_1:232;
then A1:
f /^ (1 -' 1) = f
;
assume A2:
1 <= k
; mid (f,1,k) = f | k
then
mid (f,1,k) = (f /^ (1 -' 1)) | ((k -' 1) + 1)
by Def3;
hence
mid (f,1,k) = f | k
by A2, A1, XREAL_1:235; verum