theorem Th12: :: EULRPART:12

for n being Nat
for p being one-to-one a_partition of n
for e being odd-valued a_partition of n holds
( e = Euler_transformation p iff for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )