let f be FinSequence; :: thesis: for k being Nat st 1 <= k holds
mid (f,1,k) = f | k
let k be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum