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