theorem :: RVSUM_2:26

for c1, c2 being Complex holds mlt (<*c1*>,<*c2*>) = <*(c1 * c2)*>