theorem Th6: :: EULRPART:6

for n being Nat
for p being a_partition of n ex O being odd-valued FinSequence ex a being natural-valued FinSequence st
( len O = len p & len p = len a & p = O (#) (2 |^ a) & p . 1 = (O . 1) * (2 |^ (a . 1)) & ... & p . (len p) = (O . (len p)) * (2 |^ (a . (len p))) )