theorem :: RVSUM_2:13

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