theorem :: NUMBER13:21

for f being real-valued with_values_greater_or_equal_one FinSequence holds Product f >= 1