let n, k be Nat; :: thesis: for f being FinSequence of REAL st k in dom (f /^ n) & n in dom f holds
n + k in dom f
let f be FinSequence of REAL ; :: thesis: ( k in dom (f /^ n) & n in dom f implies n + k in dom f )
assume A1: ( k in dom (f /^ n) & n in dom f ) ; :: thesis: n + k in dom f
then (len (f | n)) + k in dom ((f | n) ^ (f /^ n)) by FINSEQ_1:28;
then n + k in dom ((f | n) ^ (f /^ n)) by A1, Th10;
hence n + k in dom f by RFINSEQ:8; :: thesis: verum