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 }