let n be Nat; :: thesis: (#Z n) `| = n (#) (#Z (n - 1))
n in NAT by ORDINAL1:def 12;
hence (#Z n) `| = (n (#) (#Z (n - 1))) | ([#] REAL) by HFDIFF_1:28
.= n (#) (#Z (n - 1)) ;
:: thesis: verum