let p, q, r be complex-valued FinSequence; :: thesis: Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
thus Sum ((p ^ q) ^ r) = (Sum (p ^ q)) + (Sum r) by RVSUM_2:32
.= ((Sum p) + (Sum q)) + (Sum r) by RVSUM_2:32 ; :: thesis: verum