theorem Th2: :: NUMBER10:2

for f being integer-valued positive-yielding FinSequence holds Product f >= 1