:: by Karol P\kak

::

:: Received March 26, 2015

:: Copyright (c) 2015-2017 Association of Mizar Users

registration

let r be ext-real number ;

coherence

<*r*> is ext-real-valued

( <*r*> is decreasing & <*r*> is increasing & <*r*> is non-decreasing & <*r*> is non-increasing ) ;

end;
coherence

<*r*> is ext-real-valued

proof end;

coherence ( <*r*> is decreasing & <*r*> is increasing & <*r*> is non-decreasing & <*r*> is non-increasing ) ;

theorem Th1: :: EULRPART:1

for f, g being ext-real-valued non-decreasing FinSequence st f . (len f) <= g . 1 holds

f ^ g is non-decreasing

f ^ g is non-decreasing

proof end;

definition
end;

:: deftheorem Def1 defines odd-valued EULRPART:def 1 :

for R being Relation holds

( R is odd-valued iff rng R c= OddNAT );

for R being Relation holds

( R is odd-valued iff rng R c= OddNAT );

registration

coherence

for b_{1} being Relation st b_{1} is odd-valued holds

( b_{1} is non-zero & b_{1} is natural-valued )

end;
for b

( b

proof end;

definition

let F be Function;

( F is odd-valued iff for x being object st x in dom F holds

F . x is odd Nat )

end;
redefine attr F is odd-valued means :Def2: :: EULRPART:def 2

for x being object st x in dom F holds

F . x is odd Nat;

compatibility for x being object st x in dom F holds

F . x is odd Nat;

( F is odd-valued iff for x being object st x in dom F holds

F . x is odd Nat )

proof end;

:: deftheorem Def2 defines odd-valued EULRPART:def 2 :

for F being Function holds

( F is odd-valued iff for x being object st x in dom F holds

F . x is odd Nat );

for F being Function holds

( F is odd-valued iff for x being object st x in dom F holds

F . x is odd Nat );

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is odd-valued

coherence

<*i*> is odd-valued

end;
for b

b

proof end;

let i be odd Nat;coherence

<*i*> is odd-valued

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is OddNAT -valued holds

b_{1} is odd-valued
by RELAT_1:def 19;

end;
for b

b

definition

let n be Nat;

ex b_{1} being non-zero natural-valued non-decreasing FinSequence st Sum b_{1} = n

end;
mode a_partition of n -> non-zero natural-valued non-decreasing FinSequence means :Def3: :: EULRPART:def 3

Sum it = n;

existence Sum it = n;

ex b

proof end;

:: deftheorem Def3 defines a_partition EULRPART:def 3 :

for n being Nat

for b_{2} being non-zero natural-valued non-decreasing FinSequence holds

( b_{2} is a_partition of n iff Sum b_{2} = n );

for n being Nat

for b

( b

registration

let n be Nat;

ex b_{1} being a_partition of n st b_{1} is odd-valued

ex b_{1} being a_partition of n st b_{1} is one-to-one

end;
cluster Relation-like omega -defined RAT -valued non-zero Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued non-decreasing V294() odd-valued for a_partition of n;

existence ex b

proof end;

cluster Relation-like omega -defined RAT -valued non-zero Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued non-decreasing V294() for a_partition of n;

existence ex b

proof end;

registration

let n be Nat;

let a_{1} be set ;

a_partition of a_{1}
ex b_{1} being set st

for b_{2} being a_partition of n holds b_{2} in b_{1}

end;
let a

a_partition of a

for b

proof end;

definition

let f be odd-valued FinSequence;

ex b_{1} being valued_reorganization of f st

for n being Nat holds (2 * n) - 1 = f . (b_{1} _ (n,1)) & ... & (2 * n) - 1 = f . (b_{1} _ (n,(len (b_{1} . n))))

end;
mode odd_organization of f -> valued_reorganization of f means :Def4: :: EULRPART:def 4

for n being Nat holds (2 * n) - 1 = f . (it _ (n,1)) & ... & (2 * n) - 1 = f . (it _ (n,(len (it . n))));

existence for n being Nat holds (2 * n) - 1 = f . (it _ (n,1)) & ... & (2 * n) - 1 = f . (it _ (n,(len (it . n))));

ex b

for n being Nat holds (2 * n) - 1 = f . (b

proof end;

:: deftheorem Def4 defines odd_organization EULRPART:def 4 :

for f being odd-valued FinSequence

for b_{2} being valued_reorganization of f holds

( b_{2} is odd_organization of f iff for n being Nat holds (2 * n) - 1 = f . (b_{2} _ (n,1)) & ... & (2 * n) - 1 = f . (b_{2} _ (n,(len (b_{2} . n)))) );

for f being odd-valued FinSequence

for b

( b

theorem Th4: :: EULRPART:4

for f being odd-valued FinSequence

for o being DoubleReorganization of dom f st ( for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ) holds

o is odd_organization of f

for o being DoubleReorganization of dom f st ( for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ) holds

o is odd_organization of f

proof end;

theorem Th5: :: EULRPART:5

for i being Nat

for f being odd-valued FinSequence

for g being complex-valued FinSequence

for o1, o2 being DoubleReorganization of dom g st o1 is odd_organization of f & o2 is odd_organization of f holds

(Sum (g *. o1)) . i = (Sum (g *. o2)) . i

for f being odd-valued FinSequence

for g being complex-valued FinSequence

for o1, o2 being DoubleReorganization of dom g st o1 is odd_organization of f & o2 is odd_organization of f holds

(Sum (g *. o1)) . i = (Sum (g *. o2)) . i

proof end;

theorem Th6: :: EULRPART:6

for n being Nat

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))) )

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))) )

proof end;

theorem Th7: :: EULRPART:7

for D being finite set

for f being Function of D,NAT ex h being FinSequence of D st

for d being Element of D holds card (Coim (h,d)) = f . d

for f being Function of D,NAT ex h being FinSequence of D st

for d being Element of D holds card (Coim (h,d)) = f . d

proof end;

Lm1: for f1, f2, g1, g2 being complex-valued FinSequence st len f1 = len g1 & len f2 <= len g2 holds

(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)

proof end;

theorem Th8: :: EULRPART:8

for f1, f2, g1, g2 being complex-valued FinSequence st len f1 = len g1 holds

(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)

(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)

proof end;

Lm2: for i being Nat

for f being complex-valued FinSequence holds ((id (dom f)) (#) f) . i = i * (f . i)

proof end;

theorem Th9: :: EULRPART:9

for f, h being natural-valued FinSequence st ( for i being Nat holds card (Coim (h,i)) = f . i ) holds

Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...)

Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...)

proof end;

theorem Th10: :: EULRPART:10

for g being natural-valued FinSequence

for sort being DoubleReorganization of dom g ex h being 2 * (len b_{2}) -element FinSequence of NAT st

for j being Nat holds

( h . (2 * j) = 0 & h . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )

for sort being DoubleReorganization of dom g ex h being 2 * (len b

for j being Nat holds

( h . (2 * j) = 0 & h . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )

proof end;

Lm3: for mu being natural-valued FinSequence st ( for j being Nat holds mu . (2 * j) = 0 ) holds

ex h being odd-valued FinSequence st

( h is non-decreasing & ( for j being Nat holds card (Coim (h,j)) = mu . j ) )

proof end;

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) +...) )

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) +...) )

proof end;

definition

let n be Nat;

let p be one-to-one a_partition of n;

ex b_{1} being odd-valued a_partition of n st

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 (b_{1},1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b_{1},3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b_{1},5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b_{1},((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
by Th11;

uniqueness

for b_{1}, b_{2} being odd-valued a_partition of n st ( 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 (b_{1},1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b_{1},3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b_{1},5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b_{1},((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) & ( 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 (b_{2},1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b_{2},3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b_{2},5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b_{2},((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) holds

b_{1} = b_{2}

end;
let p be one-to-one a_partition of n;

func Euler_transformation p -> odd-valued a_partition of n means :Def5: :: EULRPART:def 5

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 (it,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (it,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (it,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (it,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) );

existence 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 (it,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (it,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (it,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (it,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) );

ex b

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 (b

uniqueness

for b

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 (b

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 (b

b

proof end;

:: deftheorem Def5 defines Euler_transformation EULRPART:def 5 :

for n being Nat

for p being one-to-one a_partition of n

for b_{3} being odd-valued a_partition of n holds

( b_{3} = Euler_transformation p iff 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 (b_{3},1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (b_{3},3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (b_{3},5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (b_{3},((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) );

for n being Nat

for p being one-to-one a_partition of n

for b

( b

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 (b

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) +... )

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) +... )

proof end;

registration

for b_{1} being real-valued Function st b_{1} is one-to-one & b_{1} is non-decreasing holds

b_{1} is increasing
end;

cluster Relation-like Function-like one-to-one real-valued non-decreasing -> real-valued increasing for set ;

coherence for b

b

proof end;

theorem Th13: :: EULRPART:13

for i being Nat

for O being odd-valued FinSequence

for a being natural-valued FinSequence

for s being odd_organization of O st len O = len a & O (#) (2 |^ a) is one-to-one holds

(a *. s) . i is one-to-one

for O being odd-valued FinSequence

for a being natural-valued FinSequence

for s being odd_organization of O st len O = len a & O (#) (2 |^ a) is one-to-one holds

(a *. s) . i is one-to-one

proof end;

Lm4: for n being Nat

for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds

rng p1 c= rng p2

proof end;

theorem Th14: :: EULRPART:14

for n being Nat

for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds

p1 = p2

for p1, p2 being one-to-one a_partition of n st Euler_transformation p1 = Euler_transformation p2 holds

p1 = p2

proof end;

theorem Th15: :: EULRPART:15

for n being Nat

for e being odd-valued a_partition of n ex p being one-to-one a_partition of n st e = Euler_transformation p

for e being odd-valued a_partition of n ex p being one-to-one a_partition of n st e = Euler_transformation p

proof end;

:: Euler's partition theorem

theorem :: EULRPART:16

for n being Nat holds card { p where p is odd-valued a_partition of n : verum } = card { p where p is one-to-one a_partition of n : verum }

proof end;