+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 as we said γ is a natural 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',
+ ρ is a transformation from R to MR',
+ and F'=G and G'=R:
+
+ (i) γ <=< φ etc are also in T