let X be ARS ; :: thesis: for x, y being Element of X st x is normform & x =*=> y holds

x = y

let x, y be Element of X; :: thesis: ( x is normform & x =*=> y implies x = y )

assume A1: x is normform ; :: thesis: ( not x =*=> y or x = y )

assume A2: x =*=> y ; :: thesis: x = y

A4: not x =+=> y by A1;

thus x = y by A2, A4, LemN; :: thesis: verum

x = y

let x, y be Element of X; :: thesis: ( x is normform & x =*=> y implies x = y )

assume A1: x is normform ; :: thesis: ( not x =*=> y or x = y )

assume A2: x =*=> y ; :: thesis: x = y

A4: not x =+=> y by A1;

thus x = y by A2, A4, LemN; :: thesis: verum