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

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