for c being Complex holds c multcomplex is_distributive_wrt addcomplex