set C = the absolutely_summable Complex_Sequence;
take the absolutely_summable Complex_Sequence ; :: thesis: the absolutely_summable Complex_Sequence is absolutely_summable
thus the absolutely_summable Complex_Sequence is absolutely_summable ; :: thesis: verum