let c1, c2, c3, c4, c5 be Complex; :: thesis: Sum <*c1,c2,c3,c4,c5*> = (((c1 + c2) + c3) + c4) + c5
Sum <*c1,c2,c3*> = (c1 + c2) + c3 by RVSUM_2:35;
then ((c1 + c2) + c3) + (c4 + c5) = (Sum <*c1,c2,c3*>) + (Sum <*c4,c5*>) by RVSUM_2:34
.= Sum <*c1,c2,c3,c4,c5*> by RVSUM_2:32 ;
hence Sum <*c1,c2,c3,c4,c5*> = (((c1 + c2) + c3) + c4) + c5 ; :: thesis: verum