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;

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

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₁ = b₂ )
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₁ = 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 ) ;

suppose x in field the reduction of X ; :: thesis: b₁ = b₂

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;

suppose not x in field the reduction of X ; :: thesis: b₁ = b₂

then ( x = b & x = c ) by A4, REWRITE1:18;
hence b = c ; :: thesis: verum

end;

end;

end;

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