let c1, c2, c3, c4 be Complex; :: thesis: Sum <*c1,c2,c3,c4*> = ((c1 + c2) + c3) + c4
thus Sum <*c1,c2,c3,c4*> = (Sum <*c1,c2,c3*>) + c4 by RVSUM_2:31
.= ((c1 + c2) + c3) + c4 by RVSUM_2:35 ; :: thesis: verum