theorem :: RVSUM_2:1

sqrcomplex is_distributive_wrt multcomplex