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 that
A1: 1 <= i and
A2: i <= k and
A3: k <= len f ; :: thesis: (mid (f,1,k)) . i = f . i
A4: i <= (k - 1) + 1 by A2;
A5: k in NAT by ORDINAL1:def 12;
A6: i in NAT by ORDINAL1:def 12;
1 <= k by A1, A2, XXREAL_0:2;
then (mid (f,1,k)) . i = f . ((i + 1) -' 1) by A1, A3, A6, A5, A4, Th128;
hence (mid (f,1,k)) . i = f . i by NAT_D:34; :: thesis: verum