theorem :: RVSUM_1:29

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