theorem :: RVSUM_2:21

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