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

(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