:: deftheorem Def4 defines odd_organization EULRPART:def 4 :
for f being odd-valued FinSequence
for b₂ being valued_reorganization of f holds
( b₂ is odd_organization of f iff for n being Nat holds (2 * n) - 1 = f . (b₂ _ (n,1)) & ... & (2 * n) - 1 = f . (b₂ _ (n,(len (b₂ . n)))) );