:: deftheorem defines * SEQ_4:def 9 :
for z being FinSequence of COMPLEX
for c being Complex holds c * z = (c multcomplex) * z;