for X being ARS
for x, y being Element of X st X is WN & X is UN* & y is_normform_of x holds
y = nf x