let n, m be Nat; :: thesis: for f being FinSequence st 1 <= m & m + n <= len f holds
(f /^ n) . m = f . (m + n)
let f be FinSequence; :: thesis: ( 1 <= m & m + n <= len f implies (f /^ n) . m = f . (m + n) )
assume that
A1: 1 <= m and
A2: m + n <= len f ; :: thesis: (f /^ n) . m = f . (m + n)
A3: (m + n) - n <= (len f) - n by A2, XREAL_1:9;
n <= n + m by NAT_1:11;
then A4: n <= len f by A2, XXREAL_0:2;
then len (f /^ n) = (len f) - n by RFINSEQ:def 1;
then m in dom (f /^ n) by A1, A3, FINSEQ_3:25;
hence (f /^ n) . m = f . (m + n) by A4, RFINSEQ:def 1; :: thesis: verum