theorem :: RVSUM_1:13

for r1, r2 being Real holds <*r1*> + <*r2*> = <*(r1 + r2)*>