Utility functions form an essential part of game theory and theoretical economics. In order to guarantee the existence of these utility functions sufficient properties are assumed in an axiomatic manner. In this paper we discuss these axioms, and a formal proof of the existence of linear utility functions. Furthermore, we consider the von-Neumann-Morgenstern Utility Theorem, its importance for game theory and economics, and a formalization thereof. The formalization includes precise definitions of the underlying concepts including continuity and independence of preferences. We make the dependencies more precise and highlight some consequences for a formalization of game theory.