+<pre>
+ (6) This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
+</pre>
+
+So for every element C1 of <b>C</b>:
+
+<pre>
+ ((M γ) -v- (unit G))[C1], by (5) =
+ M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*: G(C1)→MG'(C1) is:
+ unit[MG'(C1)] ∘ γ*, which by (6) =
+ ((unit MG') -v- γ)[C1]
+</pre>
+
+So our **(lemma 2)** is:
+
+<pre>
+ (((M γ) -v- (unit G)) = ((unit MG') -v- γ)), where γ is a transformation from G to MG'.
+</pre>
+
+
+Finally, we substitute <code>((join G') -v- (M γ) -v- φ)</code> for <code>γ <=< φ</code> in the monad laws. For simplicity, I'll omit the "-v-".
+
+<pre>
+ for all φ,γ,ρ in T, where φ is a transformation from F to MF', γ is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+
+ (i) γ <=< φ etc are also in T