theorem Th5: :: EXTREAL1:7

Sum (<*> ExtREAL) = 0.