for X being ARS
for x being Element of X st X is WN & X is UN* holds
nf (nf x) = nf x