theorem Th41: :: NUMBER08:41

for f being natural-valued finite-support Function
for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F is positive-yielding