let X be ARS ; :: thesis: for x being Element of X st X is WN & X is UN* holds

nf x is_normform_of x

let x be Element of X; :: thesis: ( X is WN & X is UN* implies nf x is_normform_of x )

assume A1: ( X is WN & X is UN* ) ; :: thesis: nf x is_normform_of x

A4: x is normalizable by A1;

A3: for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z by A1;

thus nf x is_normform_of x by A4, A3, Def17; :: thesis: verum

nf x is_normform_of x

let x be Element of X; :: thesis: ( X is WN & X is UN* implies nf x is_normform_of x )

assume A1: ( X is WN & X is UN* ) ; :: thesis: nf x is_normform_of x

A4: x is normalizable by A1;

A3: for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z by A1;

thus nf x is_normform_of x by A4, A3, Def17; :: thesis: verum