:: deftheorem defines * RVSUM_2:def 5 :
for F being complex-valued FinSequence
for c being Complex holds c * F = (c multcomplex) * F;