Definition of Function What is authoritative canonical formal definition of function?
For example,
According to Wolfram MathWorld,
$$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:


*

*Why function is not a pair in $isafun_2$? First component of triple is perfectly derivable from the second.

*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?
 A: When we use the Bourbaki definition of function as a triple (domain, codomain, graph), then two functions are usually defined to be equal iff their domains and graphs are equal. So  equal functions can have different codomains. The problem is that the same sign "=" is used both for the  the equality of functions and the "universal" equality (In ZFC, for example, the "universal" equality is defined for all sets). That is, the sign "=" is overloaded. Normally, from the context one can determine what is the intended meaning.
But there is a more serious trouble (as Vag pointed out early) with the Bourbaki definition, when a function is an element of a set. So it seems that the  definition of function as a set of ordered pairs having the functional property is more preferable.
A: 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.
