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