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