let n be Nat; :: thesis: 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))) )
let p be a_partition of n; :: thesis: 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))) )
defpred S₁[ object , object ] means for i, j being Nat st p . $1 = (2 |^ i) * ((2 * j) + 1) holds
$2 = [((2 * j) + 1),i];
A1: dom p = Seg (len p) by FINSEQ_1:def 3;
A2: for k being Nat st k in Seg (len p) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len p) implies ex x being object st S₁[k,x] )
assume k in Seg (len p) ; :: thesis: ex x being object st S₁[k,x]
then p . k in rng p by FUNCT_1:def 3, A1;
then consider n, m being Nat such that
A3: p . k = (2 |^ n) * ((2 * m) + 1) by NAGATA_2:1;
take x = [((2 * m) + 1),n]; :: thesis: S₁[k,x]
let i, j be Nat; :: thesis: ( p . k = (2 |^ i) * ((2 * j) + 1) implies x = [((2 * j) + 1),i] )
assume p . k = (2 |^ i) * ((2 * j) + 1) ; :: thesis: x = [((2 * j) + 1),i]
then ( i = n & j = m ) by A3, CARD_4:4;
hence x = [((2 * j) + 1),i] ; :: thesis: verum

end;

consider Oa being FinSequence such that
A4: ( dom Oa = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S₁[k,Oa . k] ) ) from FINSEQ_1:sch 1(A2);
deffunc H₁( object ) -> object = (Oa . $1) `1 ;
consider O being FinSequence such that
A5: ( len O = len p & ( for k being Nat st k in dom O holds
O . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A6: dom O = dom p by FINSEQ_3:29, A5;
for x being object st x in dom O holds
O . x is odd Nat

proof

let x be object ; :: thesis: ( x in dom O implies O . x is odd Nat )
assume A7: x in dom O ; :: thesis: O . x is odd Nat
then p . x in rng p by FUNCT_1:def 3, A6;
then consider n, m being Nat such that
A8: p . x = (2 |^ n) * ((2 * m) + 1) by NAGATA_2:1;
Oa . x = [((2 * m) + 1),n] by A7, A1, A8, A6, A4;
then H₁(x) = (2 * m) + 1 ;
hence O . x is odd Nat by A7, A5; :: thesis: verum

end;

then reconsider O = O as odd-valued FinSequence by Def2;
deffunc H₂( object ) -> object = (Oa . $1) `2 ;
consider A being FinSequence such that
A9: ( len A = len p & ( for k being Nat st k in dom A holds
A . k = H₂(k) ) ) from FINSEQ_1:sch 2();
A10: dom A = dom p by FINSEQ_3:29, A9;
for x being object st x in dom A holds
A . x is natural

proof

let x be object ; :: thesis: ( x in dom A implies A . x is natural )
assume A11: x in dom A ; :: thesis: A . x is natural
then p . x in rng p by FUNCT_1:def 3, A10;
then consider n, m being Nat such that
A12: p . x = (2 |^ n) * ((2 * m) + 1) by NAGATA_2:1;
Oa . x = [((2 * m) + 1),n] by A11, A1, A12, A10, A4;
then H₂(x) = n ;
hence A . x is natural by A11, A9; :: thesis: verum

end;

then reconsider A = A as natural-valued FinSequence by VALUED_0:def 12;
take O ; :: thesis: 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))) )
take A ; :: thesis: ( 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))) )
thus ( len O = len p & len p = len A ) by A5, A9; :: thesis: ( p = O (#) (2 |^ A) & p . 1 = (O . 1) * (2 |^ (A . 1)) & ... & p . (len p) = (O . (len p)) * (2 |^ (A . (len p))) )
set OA = O (#) (2 |^ A);
dom (2 |^ A) = dom A by FLEXARY1:def 4;
then A13: (dom O) /\ (dom (2 |^ A)) = dom p by A10, A6;
A14: p . 1 = (O . 1) * (2 |^ (A . 1)) & ... & p . (len p) = (O . (len p)) * (2 |^ (A . (len p)))

proof

let i be Nat; :: thesis: ( not 1 <= i or not i <= len p or p . i = (O . i) * (2 |^ (A . i)) )
assume A15: ( 1 <= i & i <= len p ) ; :: thesis: p . i = (O . i) * (2 |^ (A . i))
then i in dom p by FINSEQ_3:25;
then p . i in rng p by FUNCT_1:def 3;
then consider n, m being Nat such that
A16: p . i = (2 |^ n) * ((2 * m) + 1) by NAGATA_2:1;
( Oa . i = [((2 * m) + 1),n] & [((2 * m) + 1),n] `1 = (2 * m) + 1 & [((2 * m) + 1),n] `2 = n ) by A15, FINSEQ_3:25, A1, A16, A4;
then ( O . i = (2 * m) + 1 & A . i = n ) by A15, FINSEQ_3:25, A5, A9;
hence p . i = (O . i) * (2 |^ (A . i)) by A16; :: thesis: verum

end;

for i being Nat st i in dom p holds
p . i = (O (#) (2 |^ A)) . i

proof

let i be Nat; :: thesis: ( i in dom p implies p . i = (O (#) (2 |^ A)) . i )
assume A17: i in dom p ; :: thesis: p . i = (O (#) (2 |^ A)) . i
then ( 1 <= i & i <= len p ) by FINSEQ_3:25;
then A18: p . i = (O . i) * (2 |^ (A . i)) by A14;
(2 |^ A) . i = 2 to_power (A . i) by A17, A10, FLEXARY1:def 4;
hence p . i = (O (#) (2 |^ A)) . i by VALUED_1:5, A18; :: thesis: verum

end;

hence ( p = O (#) (2 |^ A) & p . 1 = (O . 1) * (2 |^ (A . 1)) & ... & p . (len p) = (O . (len p)) * (2 |^ (A . (len p))) ) by A13, VALUED_1:def 4, A14; :: thesis: verum