let n, k be Nat; :: thesis: for f being FinSequence of COMPLEX st k in dom (f | n) holds

k in dom f

let f be FinSequence of COMPLEX ; :: thesis: ( k in dom (f | n) implies k in dom f )

assume k in dom (f | n) ; :: thesis: k in dom f

then k in dom ((f | n) ^ (f /^ n)) by FINSEQ_2:15;

hence k in dom f by RFINSEQ:8; :: thesis: verum

k in dom f

let f be FinSequence of COMPLEX ; :: thesis: ( k in dom (f | n) implies k in dom f )

assume k in dom (f | n) ; :: thesis: k in dom f

then k in dom ((f | n) ^ (f /^ n)) by FINSEQ_2:15;

hence k in dom f by RFINSEQ:8; :: thesis: verum