theorem :: RVSUM_1:146

for F being complex-valued FinSequence holds F is FinSequence of COMPLEX by Lm5;