theorem Th72: :: RVSUM_1:72

Sum (<*> REAL) = 0 by BINOP_2:2, FINSOP_1:10;