What is authoritative canonical formal definition of function?


For example,


According to [Wolfram MathWorld](http://mathworld.wolfram.com/Function.html),
$$isafun\_1(f)\;\leftrightarrow\;
\forall a\in f\;(\exists x\exists y \;\langle x,y\rangle = a)
\; \wedge \;
\forall x\forall y\_1\forall y\_2\;((\langle x,y\_1\rangle\in f\wedge\langle x,y\_2\rangle \in f)\rightarrow y\_1=y\_2))$$


According to Bourbaki "Elements de Mathematiques, Theorie des Ensembles",
$$
isafun\_2(f)\;\leftrightarrow\;
\exists d\exists g\exists c\;(\langle d,g,c\rangle=f
\;\wedge\;isafun\_1(g)\;\wedge$$
$$\;\wedge\;
\forall x(x \in d\rightarrow \exists y(\langle x,y\rangle \in g))
\;\wedge\;
\forall x\forall y(\langle x,y\rangle \in g\rightarrow (x \in d\wedge y\in c)))
$$


How to make agree definition of function as triple with extensional equality
$$
\forall f\forall g\;[\;(isafun(f)\wedge isafun(g))
\; \rightarrow \;
[\;(\forall x(\;f(x)=g(x)\;))\leftrightarrow f=g\;]\;]
$$
?


Why such divergences in definitions exist?


Upd: Two additional questions:


1. Why function is not a pair in $isafun\_2$? First component of triple is perfectly derivable from the second.
2. What word `function` exactly means if no underlying theory is specified in context? If I build fully formal knowledge base about mathematics for automated reasoning and want to add notion of contextless function -- how I must describe it?



Definition of Function
The fact is that different subject areas of mathematics use different definitions for this basic concept. The Bourbaki definition is quite common, particularly in many of the areas well-represented here on MO, but other areas use the ordered-pair definition. 


For example, if you open any set-theory text, you will find that a function $f$ is a set of ordered pairs having the functional property that any $x$ is paired with at most one $y$, denoted $f(x)$. This definition, which is completely established and much older than the Bourbaki definition, makes a function a special kind of binary relation, which is any set of ordered pairs. The domain of a function is the set of $x$ for which $f(x)$ exists. The range is the set of all such $f(x)$, and so on. The assertion $f:A\to B$ is a statement about the *three* objects, $f$, $A$ and $B$, that $f$ is a function with domain $A$ having its range a subset of $B$. In particular, the same function $f$ can have many different codomains.


Another useful variation of the function concept is the concept of a *partial* function, common in many parts of logic, particularly set theory and computability theory. A partial function on $A$ is simply a function whose domain is included in $A$. In this case, we write $f:A\to B$, but with with *three* dots (my MO tex ability can't seem to do it), to mean that $f$ is a function with $dom(f)\subset A$ and $ran(f)\subset B$. This notion is particularly usefful in computability theory, where one has functions that might not produce an output on all input. But it also arises in set theory, where one often build partial orders consisting of small partial functions from one set to another. The union of a chain of such functions is a function again. It would be silly to insist in the Bourbaki style that there are really invisible functors running through this construction adjusting the domains and co-domains. 


One could object that the set-theorists could use the Bourbaki definition, if only they prepared better: in any context where many functions are treated, they should simply delimit an upper bound for the co-domains under consideration and use that co-domain for all the functions. But this proposal bumps into set-theoretic issues. For example, if I consider the class of all functions from an ordinal to the ordinals, then the only common co-domain is the class of all ordinals. But as this is a proper class, it isn't available if I want to consider only set functions. So there are good set-theoretic reasons not to use the Bourbaki definition.


There are numerous other basic concepts that are given different precise meanings in different subjects of mathematics. For example, the concept of *tree*. In graph theory, it is a graph with no loops, whereas in set theory, it is a kind of partial order. In finite combinatorics, it might be a finitte partial order having no diamonds, but in the infinitary theory, one often means a partial order such that the predecessors of every node are well-ordered (making the levels of the tree form a well-ordered hierarchy). The graph-theoretic definition does not allow for the cases of Souslin trees and Kurepa trees, which are central in the other theory.


There are surely numerous other examples where terminology differs.


