let n be Nat; :: thesis: 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) +... )
let p be one-to-one a_partition of n; :: thesis: 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) +... )
let e be odd-valued a_partition of n; :: thesis: ( 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) +... )
thus ( e = Euler_transformation p implies 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) +... ) :: thesis: ( ( 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) +... ) implies e = Euler_transformation p )

proof

assume A1: e = Euler_transformation p ; :: thesis: 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) +...
let O be odd-valued FinSequence; :: thesis: 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) +...
let a be natural-valued FinSequence; :: thesis: 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) +...
let sort be odd_organization of O; :: thesis: ( len O = len p & len p = len a & p = O (#) (2 |^ a) implies for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
assume A2: ( len O = len p & len p = len a & p = O (#) (2 |^ a) ) ; :: thesis: for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...
let j be Nat; :: thesis: card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...
len (2 |^ a) = len a by CARD_1:def 7;
then A3: ( dom O = dom p & dom p = dom a & dom (2 |^ a) = dom a ) by A2, FINSEQ_3:29;
reconsider S = sort as DoubleReorganization of dom p by A2, FINSEQ_3:29;
A4: (2 * 1) - 1 = 1 ;
A5: (2 * 2) - 1 = 3 ;
(2 * 3) - 1 = 5 ;
then A6: ( 1 = O . (S _ (1,1)) & ... & 1 = O . (S _ (1,(len (S . 1)))) & 3 = O . (S _ (2,1)) & ... & 3 = O . (S _ (2,(len (S . 2)))) & 5 = O . (S _ (3,1)) & ... & 5 = O . (S _ (3,(len (S . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (S _ (i,1)) & ... & (2 * i) - 1 = O . (S _ (i,(len (S . i)))) ) ) by A4, Def4, A5;
(2 |^ a) . (sort _ (j,1)) = ((2 |^ a) *. sort) _ (j,1) by FLEXARY1:42;
then card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j) . 1) + (((((2 |^ a) *. sort) . j),(1 + 1)) +...) by A6, A2, A1, Def5
.= ((((2 |^ a) *. S) . j),1) +... by FLEXARY1:20, A3 ;
hence card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... ; :: thesis: verum

end;

assume A7: 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) +... ; :: thesis: e = Euler_transformation p
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )

proof

let j be Nat; :: thesis: for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
let O be odd-valued FinSequence; :: thesis: for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
let a be natural-valued FinSequence; :: thesis: ( len O = len p & len p = len a & p = O (#) (2 |^ a) implies for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) )
assume A8: ( len O = len p & len p = len a & p = O (#) (2 |^ a) ) ; :: thesis: for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
let sort be DoubleReorganization of dom p; :: thesis: ( 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) implies ( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) )
assume A9: ( 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) ) ; :: thesis: ( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
A10: for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)

proof

let j be Nat; :: thesis: card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)
len (2 |^ a) = len a by CARD_1:def 7;
then A11: ( dom O = dom p & dom p = dom a & dom (2 |^ a) = dom a ) by A8, FINSEQ_3:29;
reconsider S = sort as DoubleReorganization of dom p ;
A12: sort is odd_organization of O by A11, A9, Th4;
(2 |^ a) . (sort _ (j,1)) = ((2 |^ a) *. sort) _ (j,1) by FLEXARY1:42;
then ((((2 |^ a) *. S) . j),1) +... = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),(1 + 1)) +...) by A11, FLEXARY1:20;
hence card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) by A12, A7, A8; :: thesis: verum

end;

( (1 * 2) - 1 = 1 & (2 * 2) - 1 = 3 & (3 * 2) - 1 = 5 ) ;
hence ( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) by A10; :: thesis: verum

end;

hence e = Euler_transformation p by Def5; :: thesis: verum