let n, m be Nat; :: thesis: for p being XFinSequence st m + n < len p holds
(p /^ n) . m = p . (m + n)
let p be XFinSequence; :: thesis: ( m + n < len p implies (p /^ n) . m = p . (m + n) )
assume A1: m + n < len p ; :: thesis: (p /^ n) . m = p . (m + n)
then A2: m < (len p) - n by XREAL_1:20;
len (p /^ n) = (len p) - n by A1, Th7, NAT_1:12;
hence (p /^ n) . m = p . (m + n) by Def2, A2, AFINSQ_1:86; :: thesis: verum