theorem :: EXTREAL1:9

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