let X be ARS ; :: thesis: for x being Element of X st ex y being Element of X st y is_normform_of x & ( for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z ) holds

nf x = nf (x, the reduction of X)

let x be Element of X; :: thesis: ( ex y being Element of X st y is_normform_of x & ( for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z ) implies nf x = nf (x, the reduction of X) )

set R = the reduction of X;

set A = the carrier of X;

F0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;

given y being Element of X such that A0: y is_normform_of x ; :: thesis: ( ex y, z being Element of X st

( y is_normform_of x & z is_normform_of x & not y = z ) or nf x = nf (x, the reduction of X) )

B0: x has_a_normal_form_wrt the reduction of X by A0, Ch2, REWRITE1:def 11;

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

y = z ; :: thesis: nf x = nf (x, the reduction of X)

then nf x is_normform_of x by A0, Def17;

then A2: nf x is_a_normal_form_of x, the reduction of X by Ch2;

y = z ) holds

nf x = nf (x, the reduction of X)

let x be Element of X; :: thesis: ( ex y being Element of X st y is_normform_of x & ( for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z ) implies nf x = nf (x, the reduction of X) )

set R = the reduction of X;

set A = the carrier of X;

F0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;

given y being Element of X such that A0: y is_normform_of x ; :: thesis: ( ex y, z being Element of X st

( y is_normform_of x & z is_normform_of x & not y = z ) or nf x = nf (x, the reduction of X) )

B0: x has_a_normal_form_wrt the reduction of X by A0, Ch2, REWRITE1:def 11;

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

y = z ; :: thesis: nf x = nf (x, the reduction of X)

then nf x is_normform_of x by A0, Def17;

then A2: nf x is_a_normal_form_of x, the reduction of X by Ch2;

now :: thesis: for b, c being object st b is_a_normal_form_of x, the reduction of X & c is_a_normal_form_of x, the reduction of X holds

b = c

hence
nf x = nf (x, the reduction of X)
by B0, A2, REWRITE1:def 12; :: thesis: verumb = c

let b, c be object ; :: thesis: ( b is_a_normal_form_of x, the reduction of X & c is_a_normal_form_of x, the reduction of X implies b_{1} = b_{2} )

assume A3: ( b is_a_normal_form_of x, the reduction of X & c is_a_normal_form_of x, the reduction of X ) ; :: thesis: b_{1} = b_{2}

then A4: ( the reduction of X reduces x,b & the reduction of X reduces x,c ) by REWRITE1:def 6;

end;assume A3: ( b is_a_normal_form_of x, the reduction of X & c is_a_normal_form_of x, the reduction of X ) ; :: thesis: b

then A4: ( the reduction of X reduces x,b & the reduction of X reduces x,c ) by REWRITE1:def 6;

per cases
( x in field the reduction of X or not x in field the reduction of X )
;

end;

suppose
x in field the reduction of X
; :: thesis: b_{1} = b_{2}

then
( b in field the reduction of X & c in field the reduction of X )
by A4, REWRITE1:19;

then reconsider y = b, z = c as Element of X by F0;

( y is_normform_of x & z is_normform_of x ) by A3, Ch2;

hence b = c by A1; :: thesis: verum

end;then reconsider y = b, z = c as Element of X by F0;

( y is_normform_of x & z is_normform_of x ) by A3, Ch2;

hence b = c by A1; :: thesis: verum