theorem :: SEQ_4:56

for c being Element of COMPLEX holds c multcomplex is_distributive_wrt addcomplex by Th54, FINSEQOP:54;