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

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