Description: The order isomorphism of the well-order R on A is a function. (Contributed by Mario Carneiro, 23-May-2015)