theorem Th40: :: NUMBER08:40

for n being Nat
for f being real-valued finite-support Function st f <= n holds
for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F <= n