for g being natural-valued FinSequence
for sort being DoubleReorganization of dom g ex h being 2 * (len b₂) -element FinSequence of NAT st
for j being Nat holds
( h . (2 * j) = 0 & h . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )