set f = seq_id CZeroseq;

now :: thesis: for n being Nat holds (|.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).|) . n = 0

let n be Nat; :: thesis: (|.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).|) . n = 0
A1: (seq_id CZeroseq) . n = 0 by Th4;
thus (|.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).|) . n = (|.(seq_id CZeroseq).| . n) * (|.(seq_id CZeroseq).| . n) by SEQ_1:8
.= (|.(seq_id CZeroseq).| . n) * |.((seq_id CZeroseq) . n).| by VALUED_1:18
.= 0 by A1, COMPLEX1:44 ; :: thesis: verum

end;

hence |.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable by COMSEQ_3:3; :: thesis: verum