thus ( X is f -unambiguous implies for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) ) :: thesis: ( ( for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) ) implies X is f -unambiguous )

proof

assume X is f -unambiguous ; :: thesis: for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 )
then f is [:X,D:] -one-to-one by DefUnambiguous1;
hence for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) by Lm3; :: thesis: verum

end;

assume for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) ; :: thesis: X is f -unambiguous
then f is [:X,D:] -one-to-one by Lm3;
hence X is f -unambiguous by DefUnambiguous1; :: thesis: verum