let c1, c2, c3 be Complex; :: thesis: Sum <*c1,c2,c3*> = (c1 + c2) + c3
thus Sum <*c1,c2,c3*> = (Sum <*c1,c2*>) + c3 by Th31
.= (c1 + c2) + c3 by Th34 ; :: thesis: verum