let X be ARS ; :: thesis: for x, y being Element of X st X is WN & X is UN* & y is_normform_of x holds
y = nf x
let x, y be Element of X; :: thesis: ( X is WN & X is UN* & y is_normform_of x implies y = nf x )
assume A1: ( X is WN & X is UN* ) ; :: thesis: ( not y is_normform_of x or y = nf x )
assume A2: y is_normform_of x ; :: thesis: y = nf x
A4: for z, u being Element of X st z is_normform_of x & u is_normform_of x holds
z = u by A1;
thus y = nf x by A2, A4, Def17; :: thesis: verum