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