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 B1: len (f /^ n) = (len f) - n by TH80b, NAT_1:12;
m < (len f) - n by A1, XREAL_1:22;
then m in dom (f /^ n) by B1, NAT_1:45;
hence (f /^ n) . m = f . (m + n) by Def2; :: thesis: verum