theorem :: RVSUM_2:5

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