theorem Th38: :: NUMBER08:38

for n being Nat
for f being natural-valued FinSequence st f <= n & f is increasing & f is positive-yielding holds
Product f divides n !