theorem Th37: :: NUMBER08:37

for f, g being ext-real-valued FinSequence st f ^ g is positive-yielding holds
( f is positive-yielding & g is positive-yielding )