MATH.2:4.4 - Define the quotient operation and show that it is well defined

When the conditions hold, form A/~, the set of classes, and define the inherited operation by:

f_bar([a1],…,[an])=[f(a1,…,an)].

The right side is independent of the chosen representatives precisely because compatible inputs return equivalent outputs. For a partial operation, agreement of domains also makes its availability independent of that choice.

This argument is reusable for unchanged conditions. The useful result is an operation on classes, together with the relation and the reason it is valid. There is no need to reproduce the proof for every subsequent calculation with the same quotient.

Preserve a representative or a way to construct one when later work needs an individual object. Knowing only a class may be sufficient for one answer and insufficient for a later request about a member.