+ similarly, ρ <=< (γ <=< φ) is:
+ ((join R') (M ρ) ((join G') (M γ) φ))
+
+ substituting these into (ii), and helping ourselves to associativity on the rhs, we get:
+ ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ)
+
+ which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ)
+
+ which by lemma 1, with ρ a transformation from G' to MR', yields:
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ)
+
+ which will be true for all ρ,γ,φ only when:
+ ((join R') (M join R')) = ((join R') (join MR')), for any R'.