{} is a_partition of 0 by RVSUM_1:72, Def3;