theorem Th6: :: EXTREAL1:8

for a being R_eal holds Sum <*a*> = a