let c, c1 be Complex; :: thesis: c * <*c1*> = <*(c * c1)*>
reconsider s = c, s1 = c1 as Element of COMPLEX by XCMPLX_0:def 2;
s * <*s1*> = <*((multcomplex [;] (s,(id COMPLEX))) . s1)*> by FINSEQ_2:35
.= <*(c * c1)*> by Lm1 ;
hence c * <*c1*> = <*(c * c1)*> ; :: thesis: verum