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

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