This result follows directly from the definition using result R4041: Commutativity of finite basic real summation for two sums. $\square$