theorem Th28: :: HFDIFF_1:28

for n being Element of NAT
for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z