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