theorem Th5: :: EXTREAL1:7
Sum (<*> ExtREAL) = 0.