In the early 1960s, by using techniques from the model theory of first-order logic, Robinson gave a rigorous formulation and extension of Leibniz' infinitesimal calculus. Since then, the methodology has found applications in a wide spectrum of areas in mathematics, with particular success in the probability theory and functional analysis. In the latter, fruitful results were produced with Luxemburg's invention of the nonstandard hull construction. However, there is still no publication of a coherent and self-contained treatment of functional analysis using methods from nonstandard analysis. This publication aims to fill this gap.