let n be Nat; :: thesis:
let d be one-to-one a_partition of n; :: thesis:
consider O being odd-valued FinSequence, a being natural-valued FinSequence such that
A1: ( len O = len d & len d = len a & d = O (#) (2 |^ a) ) and
d . 1 = (O . 1) * (2 |^ (a . 1)) & ... & d . (len d) = (O . (len d)) * (2 |^ (a . (len d))) by Th6;
len (2 |^ a) = len O by A1, CARD_1:def 7;
then reconsider sort = the odd_organization of O as DoubleReorganization of dom (2 |^ a) by FINSEQ_3:29;
consider mu being 2 * (len sort) -element FinSequence of NAT such that
A2: for j being Nat holds
( mu . (2 * j) = 0 & mu . ((2 * j) - 1) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) by Th10;
set alpha = a * (sort . 1);
set beta = a * (sort . 2);
set gamma = a * (sort . 3);
A3: n = ((((((2 |^ (a * (sort . 1))) . 1) + (((2 |^ (a * (sort . 1))),2) +...)) * 1) + ((((2 |^ (a * (sort . 2))) . 1) + (((2 |^ (a * (sort . 2))),2) +...)) * 3)) + ((((2 |^ (a * (sort . 3))) . 1) + (((2 |^ (a * (sort . 3))),2) +...)) * 5)) + ((((id (dom mu)) (#) mu),7) +...)

reconsider o1 = sort as DoubleReorganization of dom d by A1, FINSEQ_3:29;
A4: ( dom (d *. o1) = dom o1 & dom ((2 |^ a) *. sort) = dom sort ) by FOMODEL2:def 6;
A5: for j being Nat holds Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1))

let j be Nat; :: thesis:
A6: mu . ((2 * j) - 1) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) by A2;

per cases ;

suppose j in dom o1 ; :: thesis:

set jj = (2 * j) - 1;
A7: (d *. o1) . j = d * (o1 . j) by FLEXARY1:41;
A8: ((2 |^ a) *. sort) . j = (2 |^ a) * (sort . j) by FLEXARY1:41;
A9: len ((d *. o1) . j) = len (o1 . j) by CARD_1:def 7;
A10: len (((2 |^ a) *. sort) . j) = len (sort . j) by CARD_1:def 7;
for n being Nat st 1 <= n & n <= len (sort . j) holds
((d *. o1) . j) . n = (((2 * j) - 1) * (((2 |^ a) *. sort) . j)) . n

proof

let n be Nat; :: thesis:
assume A11: ( 1 <= n & n <= len (sort . j) ) ; :: thesis:
A12: (2 * j) - 1 = O . (o1 _ (j,1)) & ... & (2 * j) - 1 = O . (o1 _ (j,(len (o1 . j)))) by Def4;
thus ((d *. o1) . j) . n = d . (o1 _ (j,n)) by A11, A9, FINSEQ_3:25, A7, FUNCT_1:12
.= (O . (o1 _ (j,n))) * ((2 |^ a) . (o1 _ (j,n))) by A1, VALUED_1:5
.= ((2 * j) - 1) * ((2 |^ a) . (o1 _ (j,n))) by A12, A11
.= ((2 * j) - 1) * ((((2 |^ a) *. sort) . j) . n) by A11, A10, FINSEQ_3:25, A8, FUNCT_1:12
.= (((2 * j) - 1) * (((2 |^ a) *. sort) . j)) . n by VALUED_1:6 ; :: thesis:

end;

then A13: (d *. o1) . j = ((2 * j) - 1) * (((2 |^ a) *. sort) . j) by A9, CARD_1:def 7;
(((2 |^ a) *. sort) . j) . 1 = ((2 |^ a) *. sort) _ (j,1) ;
then (2 |^ a) . (sort _ (j,1)) = (((2 |^ a) *. sort) . j) . 1 by FLEXARY1:42;
then Sum (((2 |^ a) *. sort) . j) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) by FLEXARY1:22
.= mu . ((2 * j) - 1) by A2 ;
hence Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1)) by A13, RVSUM_1:87; :: thesis:

end;

suppose A14: not j in dom sort ; :: thesis:

then sort . j = {} by FUNCT_1:def 2;
then A15: not (sort . j) . 1 in dom (2 |^ a) by FINSEQ_3:25;
not j in dom ((2 |^ a) *. sort) by A14, FOMODEL2:def 6;
then ((2 |^ a) *. sort) . j = {} by FUNCT_1:def 2;
then ((((2 |^ a) *. sort) . j),2) +... = 0 by FLEXARY1:15;
then mu . ((2 * j) - 1) = 0 by A6, A15, FUNCT_1:def 2;
hence Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1)) by A14, A4, FUNCT_1:def 2, RVSUM_1:72; :: thesis:

end;

set I = idseq (len mu);
A16: idseq (len mu) = id (dom mu) by FINSEQ_1:def 3;
A17: ( 1 -' 1 = 0 & 2 -' 1 = 2 - 1 ) by XREAL_1:233, XREAL_1:232;
A18: for j being Nat holds ((Sum (d *. o1)),(4 + (j * 1))) +...+ ((Sum (d *. o1)),((4 + (j * 1)) + (1 -' 1))) = (((idseq (len mu)) (#) mu),(7 + (j * 2))) +...+ (((idseq (len mu)) (#) mu),((7 + (j * 2)) + (2 -' 1)))

proof

let j be Nat; :: thesis:
set S = Sum (d *. o1);
A19: ((Sum (d *. o1)),(4 + (j * 1))) +...+ ((Sum (d *. o1)),((4 + (j * 1)) + (1 -' 1))) = (Sum (d *. o1)) . (4 + j) by A17, FLEXARY1:11
.= Sum ((d *. o1) . (4 + j)) by FLEXARY1:def 8
.= ((2 * (4 + j)) - 1) * (mu . ((2 * (4 + j)) - 1)) by A5
.= ((2 * j) + 7) * (mu . ((2 * j) + 7)) ;
A20: (((idseq (len mu)) (#) mu),(7 + (j * 2))) +...+ (((idseq (len mu)) (#) mu),((7 + (j * 2)) + (2 -' 1))) = (((idseq (len mu)) (#) mu) . (7 + (j * 2))) + ((((idseq (len mu)) (#) mu),((7 + (j * 2)) + 1)) +...+ (((idseq (len mu)) (#) mu),((7 + (j * 2)) + 1))) by NAT_1:11, FLEXARY1:13, A17
.= (((idseq (len mu)) (#) mu) . (7 + (j * 2))) + (((idseq (len mu)) (#) mu) . ((7 + (j * 2)) + 1)) by FLEXARY1:11 ;
(7 + (j * 2)) + 1 = 2 * (j + 4) ;
then mu . ((7 + (j * 2)) + 1) = 0 by A2;
then ((idseq (len mu)) (#) mu) . ((7 + (j * 2)) + 1) = ((7 + (j * 2)) + 1) * 0 by A16, Lm2;
hence ((Sum (d *. o1)),(4 + (j * 1))) +...+ ((Sum (d *. o1)),((4 + (j * 1)) + (1 -' 1))) = (((idseq (len mu)) (#) mu),(7 + (j * 2))) +...+ (((idseq (len mu)) (#) mu),((7 + (j * 2)) + (2 -' 1))) by A19, A20, A16, Lm2; :: thesis:

end;

A21: ((Sum (d *. o1)),4) +... = (((idseq (len mu)) (#) mu),7) +... from FLEXARY1:sch 1(A18);
A22: (2 * 1) - 1 = 1 ;
then A23: 1 * (mu . 1) = Sum ((d *. o1) . 1) by A5
.= (Sum (d *. o1)) . 1 by FLEXARY1:def 8 ;
A24: (2 * 2) - 1 = 3 ;
then A25: 3 * (mu . 3) = Sum ((d *. o1) . 2) by A5
.= (Sum (d *. o1)) . 2 by FLEXARY1:def 8 ;
A26: (2 * 3) - 1 = 5 ;
then A27: 5 * (mu . 5) = Sum ((d *. o1) . 3) by A5
.= (Sum (d *. o1)) . 3 by FLEXARY1:def 8 ;
for j being Nat holds
( (2 |^ a) . (sort _ (j,1)) = (2 |^ (a * (sort . j))) . 1 & ((2 |^ a) *. sort) . j = 2 |^ (a * (sort . j)) )

proof

end;

then A29: ( (2 |^ a) . (sort _ (1,1)) = (2 |^ (a * (sort . 1))) . 1 & (2 |^ a) . (sort _ (2,1)) = (2 |^ (a * (sort . 2))) . 1 & (2 |^ a) . (sort _ (3,1)) = (2 |^ (a * (sort . 3))) . 1 & ((2 |^ a) *. sort) . 1 = 2 |^ (a * (sort . 1)) & ((2 |^ a) *. sort) . 2 = 2 |^ (a * (sort . 2)) & ((2 |^ a) *. sort) . 3 = 2 |^ (a * (sort . 3)) ) ;
thus n = Sum d by Def3
.= Sum (Sum (d *. o1)) by FLEXARY1:47
.= (1 * (mu . 1)) + (((Sum (d *. o1)),2) +...) by FLEXARY1:22, A23
.= (1 * (mu . 1)) + ((3 * (mu . 3)) + (((Sum (d *. o1)),(2 + 1)) +...)) by A25, FLEXARY1:20
.= ((1 * (mu . 1)) + (3 * (mu . 3))) + (((Sum (d *. o1)),3) +...)
.= ((1 * (mu . 1)) + (3 * (mu . 3))) + ((5 * (mu . 5)) + (((Sum (d *. o1)),(3 + 1)) +...)) by FLEXARY1:20, A27
.= (((1 * (mu . 1)) + (3 * (mu . 3))) + (5 * (mu . 5))) + ((((id (dom mu)) (#) mu),7) +...) by A16, A21
.= (((1 * (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...))) + (3 * (mu . 3))) + (5 * (mu . 5))) + ((((id (dom mu)) (#) mu),7) +...) by A2, A22
.= (((1 * (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...))) + (3 * (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...)))) + (5 * (mu . 5))) + ((((id (dom mu)) (#) mu),7) +...) by A2, A24
.= ((((((2 |^ (a * (sort . 1))) . 1) + (((2 |^ (a * (sort . 1))),2) +...)) * 1) + ((((2 |^ (a * (sort . 2))) . 1) + (((2 |^ (a * (sort . 2))),2) +...)) * 3)) + ((((2 |^ (a * (sort . 3))) . 1) + (((2 |^ (a * (sort . 3))),2) +...)) * 5)) + ((((id (dom mu)) (#) mu),7) +...) by A2, A26, A29 ; :: thesis:

end;

A30: n = ((((mu . 1) * 1) + ((mu . 3) * 3)) + ((mu . 5) * 5)) + ((((id (dom mu)) (#) mu),7) +...)

proof

for j being Nat holds
( (2 |^ a) . (sort _ (j,1)) = (2 |^ (a * (sort . j))) . 1 & ((2 |^ a) *. sort) . j = 2 |^ (a * (sort . j)) )

proof

end;

end;

consider h being odd-valued FinSequence such that
A35: ( h is non-decreasing & ( for i being Nat holds card (Coim (h,i)) = mu . i ) ) by Lm3, A2;
A36: n = ((((card (Coim (h,1))) * 1) + ((card (Coim (h,3))) * 3)) + ((card (Coim (h,5))) * 5)) + ((((id (dom mu)) (#) mu),7) +...)

proof

A37: mu . 1 = card (Coim (h,1)) by A35;
mu . 3 = card (Coim (h,3)) by A35;
hence n = ((((card (Coim (h,1))) * 1) + ((card (Coim (h,3))) * 3)) + ((card (Coim (h,5))) * 5)) + ((((id (dom mu)) (#) mu),7) +...) by A35, A37, A30; :: thesis:

end;

n = Sum h

proof

set I = idseq (len mu);
A38: idseq (len mu) = id (dom mu) by FINSEQ_1:def 3;
then ((idseq (len mu)) (#) mu) . 3 = 3 * (mu . 3) by Lm2;
then A39: (((idseq (len mu)) (#) mu),3) +... = (3 * (mu . 3)) + ((((idseq (len mu)) (#) mu),(3 + 1)) +...) by FLEXARY1:20
.= (3 * (card (Coim (h,3)))) + ((((idseq (len mu)) (#) mu),(3 + 1)) +...) by A35 ;
A40: ( ((idseq (len mu)) (#) mu) . 4 = 4 * (mu . 4) & 4 = 2 * 2 ) by A38, Lm2;
then mu . 4 = 0 by A2;
then A41: (((idseq (len mu)) (#) mu),4) +... = 0 + ((((idseq (len mu)) (#) mu),(4 + 1)) +...) by A40, FLEXARY1:20;
((idseq (len mu)) (#) mu) . 5 = 5 * (mu . 5) by A38, Lm2;
then A42: (((idseq (len mu)) (#) mu),5) +... = (5 * (mu . 5)) + ((((idseq (len mu)) (#) mu),(5 + 1)) +...) by FLEXARY1:20
.= (5 * (card (Coim (h,5)))) + ((((idseq (len mu)) (#) mu),(5 + 1)) +...) by A35 ;
A43: ( ((idseq (len mu)) (#) mu) . 6 = 6 * (mu . 6) & 6 = 3 * 2 ) by A38, Lm2;
then mu . 6 = 0 by A2;
then A44: (((idseq (len mu)) (#) mu),6) +... = 0 + ((((idseq (len mu)) (#) mu),(6 + 1)) +...) by A43, FLEXARY1:20;
2 * 1 = 2 ;
then mu . 2 = 0 by A2;
then 2 * (mu . 2) = 0 ;
hence Sum h = ((1 * (mu . 1)) + 0) + ((((id (dom mu)) (#) mu),3) +...) by Th9, A35
.= (1 * (card (Coim (h,1)))) + ((((id (dom mu)) (#) mu),3) +...) by A35
.= n by A36, A39, A41, A38, A42, A44 ;
:: thesis:

end;

then reconsider h = h as odd-valued a_partition of n by A35, Def3;
take h ; :: thesis:
let j be Nat; :: thesis:
let O1 be odd-valued FinSequence; :: thesis:
let a1 be natural-valued FinSequence; :: thesis:
assume A45: ( len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) ) ; :: thesis:
let sort1 be DoubleReorganization of dom d; :: thesis:
assume A46: ( 1 = O1 . (sort1 _ (1,1)) & ... & 1 = O1 . (sort1 _ (1,(len (sort1 . 1)))) & 3 = O1 . (sort1 _ (2,1)) & ... & 3 = O1 . (sort1 _ (2,(len (sort1 . 2)))) & 5 = O1 . (sort1 _ (3,1)) & ... & 5 = O1 . (sort1 _ (3,(len (sort1 . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort1 _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort1 _ (i,(len (sort1 . i)))) ) ) ; :: thesis:
for j being Nat st 1 <= j & j <= len d holds
( O . j = O1 . j & a . j = a1 . j )

proof

let j be Nat; :: thesis:
assume A48: ( 1 <= j & j <= len d ) ; :: thesis:
A49: (O1 . j) * ((2 |^ a1) . j) = (O1 (#) (2 |^ a1)) . j by VALUED_1:5
.= (O . j) * ((2 |^ a) . j) by VALUED_1:5, A1, A45 ;
j in dom a by A48, FINSEQ_3:25, A1;
then A50: (2 |^ a) . j = 2 to_power (a . j) by FLEXARY1:def 4
.= 2 |^ (a . j) ;
j in dom a1 by A48, FINSEQ_3:25, A45;
then A51: (2 |^ a1) . j = 2 to_power (a1 . j) by FLEXARY1:def 4
.= 2 |^ (a1 . j) ;
j in dom O by A48, FINSEQ_3:25, A1;
then O . j is odd Nat by Def2;
then consider i1 being Nat such that
A52: O . j = (2 * i1) + 1 by ABIAN:9;
j in dom O1 by A48, FINSEQ_3:25, A45;
then O1 . j is odd Nat by Def2;
then ex i2 being Nat st O1 . j = (2 * i2) + 1 by ABIAN:9;
hence ( O . j = O1 . j & a . j = a1 . j ) by A50, A51, A52, A49, CARD_4:4; :: thesis:

end;

then A53: ( O = O1 & a = a1 ) by A45, A1;
A54: for j being Nat holds card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...)

proof

let j be Nat; :: thesis:
A55: (2 |^ a) . (sort _ (j,1)) = ((2 |^ a) *. sort) _ (j,1) by FLEXARY1:42;
A56: len (2 |^ a) = len a by CARD_1:def 7;
then A57: ( dom O = dom d & dom d = dom a & dom (2 |^ a) = dom a ) by A1, FINSEQ_3:29;
card (Coim (h,((j * 2) - 1))) = mu . ((2 * j) - 1)

proof

per cases ;

suppose A58: j = 0 ; :: thesis:

then A59: not (2 * j) - 1 in dom mu ;
not (2 * j) - 1 in rng h by A58;
then h " {((2 * j) - 1)} = {} by FUNCT_1:72;
then Coim (h,((j * 2) - 1)) = {} by RELAT_1:def 17;
hence card (Coim (h,((j * 2) - 1))) = mu . ((2 * j) - 1) by A59, FUNCT_1:def 2; :: thesis:

end;

suppose j > 0 ; :: thesis:

hence card (Coim (h,((j * 2) - 1))) = mu . ((2 * j) - 1) by A35; :: thesis:

end;

then A60: card (Coim (h,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j) . 1) + (((((2 |^ a) *. sort) . j),2) +...) by A2, A55
.= Sum (((2 |^ a) *. sort) . j) by FLEXARY1:22 ;
reconsider S = sort1 as DoubleReorganization of dom (2 |^ a) by A56, A1, FINSEQ_3:29;
(2 |^ a1) . (sort1 _ (j,1)) = ((2 |^ a1) *. sort1) _ (j,1) by FLEXARY1:42;
then A61: ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) = Sum (((2 |^ a) *. S) . j) by A53, FLEXARY1:22;
A62: sort1 is odd_organization of O by A57, Th4, A46, A53;
thus card (Coim (h,((j * 2) - 1))) = (Sum ((2 |^ a) *. sort)) . j by FLEXARY1:def 8, A60
.= (Sum ((2 |^ a) *. S)) . j by A62, Th5
.= ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) by FLEXARY1:def 8, A61 ; :: thesis:

end;

( (2 * 1) - 1 = 1 & (2 * 2) - 1 = 3 & (2 * 3) - 1 = 5 ) ;
hence ( card (Coim (h,1)) = ((2 |^ a1) . (sort1 _ (1,1))) + (((((2 |^ a1) *. sort1) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort1 _ (2,1))) + (((((2 |^ a1) *. sort1) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort1 _ (3,1))) + (((((2 |^ a1) *. sort1) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) ) by A54; :: thesis: