Step * 1 of Lemma mon_for_of_op


1. IAbMonoid
2. Type
3. A ⟶ |g|
4. A ⟶ |g|
⊢ (e e) ∈ |g|
BY
(RW AbMonNormC THEN Auto) }


Latex:


Latex:

1.  g  :  IAbMonoid
2.  A  :  Type
3.  e  :  A  {}\mrightarrow{}  |g|
4.  f  :  A  {}\mrightarrow{}  |g|
\mvdash{}  e  =  (e  *  e)


By


Latex:
(RW  AbMonNormC  0  THEN  Auto)




Home Index