theorem Th19: :: NUMBER13:19

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