theorem :: NUMBER08:42

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 one-to-one