Grothendieck Construction

I'm looking for a reference where a theorem of this form was first proven:

If (C,⊗_C) is (symmetric) monoidal, F: C -> Cat a lax (symmetric) monoidal functor, and μ the associated natural transformation, then the Grothendieck category of F is (symmetric) monoidal with ⊗ defined by (c,x)⊗(d,y)=(c⊗d,μ_c,d(x,y)).

The proof is a straightforward verification, so I expect it has been done before. thanks, Joe Moeller [For admin and other information see: http://www.mta.ca/~cat-dist/ ]