let c be Complex; :: thesis: c multcomplex is_distributive_wrt addcomplex
c in COMPLEX by XCMPLX_0:def 2;
hence c multcomplex is_distributive_wrt addcomplex by FINSEQOP:54, SEQ_4:54; :: thesis: verum