let X be ARS ; 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; ( 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
; ( 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
; 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;
hence
nf x = nf (x, the reduction of X)
by B0, A2, REWRITE1:def 12; verum