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