for n being Nat holds (#Z n) `| = n (#) (#Z (n - 1))