let m, n 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, Th16, NAT_1:12;
then m in dom (p /^ n) by A2, NAT_1:44;
hence (p /^ n) . m = p . (m + n) by Def2; :: thesis: verum