let D be non empty set ; :: thesis: for f being FinSequence of D
for k, i being Nat st 1 <= i & i <= k & k <= len f holds
(mid f,1,k) . i = f . i
let f be FinSequence of D; :: thesis: for k, i being Nat st 1 <= i & i <= k & k <= len f holds
(mid f,1,k) . i = f . i
let k, i be Nat; :: thesis: ( 1 <= i & i <= k & k <= len f implies (mid f,1,k) . i = f . i )
assume A1: ( 1 <= i & i <= k & k <= len f ) ; :: thesis: (mid f,1,k) . i = f . i
then A2: ( 1 <= k & k <= len f & 1 <= i & i <= k ) by XXREAL_0:2;
X: ( i in NAT & k in NAT ) by ORDINAL1:def 13;
i <= (k - 1) + 1 by A1;
then (mid f,1,k) . i = f . ((i + 1) -' 1) by A2, Th31, X;
hence (mid f,1,k) . i = f . i by NAT_D:34; :: thesis: verum