for seq1, seq2 being Real_Sequence st seq1 is absolutely_summable & seq2 is summable holds
( seq1 (##) seq2 is summable & Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) )