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