The theory of functions in TLAPS (more precisely, in the Isabelle backend of TLAPS, which we consider as the standard), is axiomatized in precisely this way, plus the related definitions of [S -> T] and the EXCEPT construct. I'd therefore object to your assertion that the theory is defined semantically rather than axiomatically.