theorem :: HILB10_4:6

for c1, c2 being Complex holds Product <%c1,c2%> = c1 * c2