let r1, r2, r3 be Complex; :: thesis: Product <*r1,r2,r3*> = (r1 * r2) * r3
thus Product <*r1,r2,r3*> = (Product <*r1,r2*>) * r3 by Th96
.= (r1 * r2) * r3 by Th99 ; :: thesis: verum