let p, q, r be FinSequence of INT ; :: thesis: Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
Sum ((p ^ q) ^ r) = (Sum (p ^ q)) + (Sum r) by RVSUM_1:75
.= ((Sum p) + (Sum q)) + (Sum r) by RVSUM_1:75 ;
hence Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r) ; :: thesis: verum