:: deftheorem defines seq_const RVSUM_4:def 1 :
for c being Complex holds seq_const c = NAT --> c;