theorem :: COMSEQ_3:73

for seq being Complex_Sequence
for p being Real st p > 1 & ( for n being Nat st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) holds
seq is absolutely_summable by SERIES_1:32;