let f be XFinSequence; :: thesis: for n, m being Nat st m + n < len f holds
(f /^ n) . m = f . (m + n)
let n, m be Nat; :: thesis: ( m + n < len f implies (f /^ n) . m = f . (m + n) )
assume A1: m + n < len f ; :: thesis: (f /^ n) . m = f . (m + n)
then A2: m < (len f) - n by XREAL_1:22;
len (f /^ n) = (len f) - n by A1, Th16, NAT_1:12;
then m in dom (f /^ n) by A2, NAT_1:45;
hence (f /^ n) . m = f . (m + n) by Def2; :: thesis: verum