let R be weakly-normalizing with_UN_property Relation; :: thesis: for a, b being set st a,b are_convertible_wrt R holds
nf (a,R) = nf (b,R)
let a, b be set ; :: 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 Th55;
then A2: nf (b,R) is_a_normal_form_wrt R by Def6;
R reduces b, nf (b,R) by A1, Def6;
then A3: b, nf (b,R) are_convertible_wrt R by Th26;
A4: nf (a,R) is_a_normal_form_of a,R by Th55;
then R reduces a, nf (a,R) by Def6;
then A5: nf (a,R),a are_convertible_wrt R by Th26;
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, Th31;
then A6: nf (a,R), nf (b,R) are_convertible_wrt R by A3, Th31;
nf (a,R) is_a_normal_form_wrt R by A4, Def6;
hence nf (a,R) = nf (b,R) by A2, A6, Def19; :: thesis: verum