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

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