theorem Th4: :: EULRPART:4

for f being odd-valued FinSequence
for o being DoubleReorganization of dom f st ( for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ) holds
o is odd_organization of f