theorem Th54: :: SEQ_4:54

multcomplex is_distributive_wrt addcomplex