theorem Th9: :: HILB10_4:9

for c1, c2 being Complex holds c1 + <%c2%> = <%(c1 + c2)%>