let R be weakly-normalizing with_UN_property Relation; :: thesis: for a, b being object st a,b are_convertible_wrt R holds
nf (a,R) = nf (b,R)
let a, b be object ; :: thesis: ( a,b are_convertible_wrt R implies nf (a,R) = nf (b,R) )
A1: nf (b,R) is_a_normal_form_of b,R by Th54;
then A2: nf (b,R) is_a_normal_form_wrt R ;
R reduces b, nf (b,R) by A1;
then A3: b, nf (b,R) are_convertible_wrt R by Th25;
A4: nf (a,R) is_a_normal_form_of a,R by Th54;
then R reduces a, nf (a,R) ;
then A5: nf (a,R),a are_convertible_wrt R by Th25;
assume a,b are_convertible_wrt R ; :: thesis: nf (a,R) = nf (b,R)
then nf (a,R),b are_convertible_wrt R by A5, Th30;
then A6: nf (a,R), nf (b,R) are_convertible_wrt R by A3, Th30;
nf (a,R) is_a_normal_form_wrt R by A4;
hence nf (a,R) = nf (b,R) by A2, A6, Def19; :: thesis: verum