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