This is a reference request for the following "well-known" theorems in category theory:

1) There is an equivalence of categories between finitary monads on $\mathbf{Set}$ and finitary Lawvere theories (i.e. single-sorted finite product theories).

2) There is an equivalence of categories between monads on $\mathbf{Set}$ and infinitary Lawvere theories (i.e. singled-sorted product theories).

3) The category of models of a finitary/infinitary Lawvere theory is equivalent to the category of algebras of the corresponding monad.
 
I am not looking for proofs (I have written them up). I am looking for references *which actually give proofs*, so that I can cite them in a paper (instead of writing up the proof in the paper). Ideally, they should be classical references. I have scrolled through lots of papers which mention the theorems, and most of the time one (or several) of Linton's papers (let's give them letters) are cited:
 
- **E.** *Some aspects of equational theories*, Proceedings of the Conference on Categorical
Algebra, Springer, 1966
- **F.** *An outline of functorial semantics*, Seminar on triples and categorical homology theory,
Springer, 1969
- **A.** *Applied functorial semantics*, Seminar on triples and categorical homology theory,
Springer, 1969
 
Sometimes, also the book "Toposes, Triples and Theories" by Barr & Wells is cited.
 
In **E** Linton only mentions 2) in the end of section 6, without proof. In fact, Linton proves a characterization theorem of the concrete categories of models of varietal theories (his name for infinitary Lawvere theories), via a version of the first isomorphism theorem, and he only mentions in passing that a combination with Beck's monadicity theorem yields the
equivalence to monads (but this detour is actually not necessary to get the equivalence; so this is not the simplest proof anyway).

I do not understand much what is going on in **F** (I find it very hard to read, also because of the typesetting and the chaotic structure), but it seems to deal with a *much* more general situation, and therefore I don't see where 1) or 2) is proven either. This is funny because both in the introduction of the Lecture Notes and in the introduction of **A** it is claimed that Linton proves 2) in **F**. Can perhaps someone help me to "decipher" **F** and explain where 2) is actually proved? The only result which looks similar is Lemma 10.2, but its proof is omitted... Maybe 3) follows from Theorem 9.3, but I don't see how.

The paper **A** focusses on monadicity criterions, and just mentions 2) in the introduction.

I could not find a proof in the book by Barr-Wells either. They talk about the history of these theorems in section 4.5 and attribute 1) and 2) to Linton's **E** and **F**.
 
I have found references with proofs of more general versions of 1), for example in the enriched case (Nishizawa, Power, *Lawvere theories enriched over a general base*), but it is probably awkward to cite such a paper for a classical result. I haven't found a published proof of 2) so far. The only thing which comes very close to 2) and 3) is the nlab article on algebraic theories: https://ncatlab.org/nlab/show/algebraic+theory, but the proof is sketchy.