- φ is a transformation from F to MF', so:
- unit <=< φ becomes: (join F') (M φ) unit
- substituting in (iii.2), we get:
- φ = ((join F') (M φ) (unit F))
- --------------
- which by lemma (2), yields:
- ------------
- φ = ((join F') ((unit MF') φ)
-
- which will be true for all φ just in case:
-
- ((join F') (unit MF')) = the identity transformation, for any F'
-
- which will in turn be true just in case:
-
+ unit <=< γ becomes: ((join R'G) (M γ) unit)
+
+ substituting in (iii.2), we get:
+ γ = ((join R'G) (M γ) (unit G))
+
+ which by lemma 2, yields:
+ γ = ((join R'G) ((unit MR'G) γ)
+
+ which will be true for all γ just in case:
+ ((join R'G) (unit MR'G)) = the identity transformation, for any R'G
+
+ which will in turn be true just in case: