Description: The closure of an operation outside its domain, when the domain
includes the empty set. This technical lemma can make the operation
more convenient to work in some cases. It is dependent on our
particular definitions of operation value, function value, and ordered
pair. (Contributed by NM, 24-Sep-2004)