theorem :: RVSUM_1:1

0 is_a_unity_wrt addreal by BINOP_2:2, SETWISEO:14;