let D be non empty set ; :: thesis: for f being FinSequence of D
for k being Nat st 1 <= k holds
mid (f,1,k) = f | k
let f be FinSequence of D; :: 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:234;
then A1: f /^ (1 -' 1) = f by FINSEQ_5:31;
assume A2: 1 <= k ; :: thesis: mid (f,1,k) = f | k
then mid (f,1,k) = (f /^ (1 -' 1)) | ((k -' 1) + 1) by Def1;
hence mid (f,1,k) = f | k by A2, A1, XREAL_1:237; :: thesis: verum