theorem Th13: :: POLYDIFF:13

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