Update the functions_def axiom in numbers/sets/functions sub-theory package to more carefully specify functions with domain A and codomain B instead of functions that take A to B but might also have elements outside of A in their domain.

Add UNDEF literal, a common expression labeled as 'undefined' in logic/sets/functions, most immediately for use in the expression of function-related expressions where the function is not defined for some set of inputs. This is then used in an update to the functions_def axiomatic definition of sets/functions and related theorems.

Update the functions_def axiom in logic/sets/functions to utilize the UNDEF literal for undefined function outputs and establish the Restriction() class in logic/sets/functions along with related axiomatic definition, a related theorem, and some entries in the logic/sets/functions demonstrations notebook.

Add comment in Restriction() class description for future consideration, possibly changing Restriction(f, S) to Restriction(f, A, B, S) to include the original domain and co-domain of the function f (since neither may be easily accessible from the Restriction(f, S) construction itself).