let f be FinSequence; :: 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;
1 <= k by A1, A2, XXREAL_0:2;
then (mid (f,1,k)) . i = f . ((i + 1) -' 1) by A1, A3, A4, Th121;
hence (mid (f,1,k)) . i = f . i by NAT_D:34; :: thesis: verum