theorem :: RVSUM_4:22

for f being complex-valued XFinSequence holds Sequel f = f ^ (seq_const 0)