theorem Th11: :: EULRPART:11

for n being Nat
for d being one-to-one a_partition of n ex e being odd-valued a_partition of n st
for j being Nat
for O1 being odd-valued FinSequence
for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )