consider C being absolutely_summable Complex_Sequence;
take C ; :: thesis: C is absolutely_summable
thus C is absolutely_summable ; :: thesis: verum