Description: The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015)