let r1, r2 be complex number ; :: thesis: Product <*r1,r2*> = r1 * r2
thus Product <*r1,r2*> = (Product <*r1*>) * r2 by Th126
.= r1 * r2 by Th125 ; :: thesis: verum