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