theorem :: AFINSQ_2:54

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