theorem Th43: :: NUMBER08:43

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