:: deftheorem defines Sequel RVSUM_4:def 8 :
for f being complex-valued XFinSequence holds Sequel f = (NAT --> 0) +* f;