for a, b being R_eal holds Sum <*a,b*> = a + b