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