theorem Th64: :: MEASUR12:64

for F, G being FinSequence of ExtREAL holds
( ( F is without-infty & G is without-infty implies F ^ G is without-infty ) & ( F is without+infty & G is without+infty implies F ^ G is without+infty ) )