Step * of Lemma munit_char

g:IAbMonoid. ∀a:|g|.  (g-unit(a) ⇐⇒ e)
BY
((Unfold `munit` THEN GenRepD THENA Auto) }

1
1. IAbMonoid@i'
2. |g|@i
3. e
⊢ e

2
1. IAbMonoid@i'
2. |g|@i
3. e
⊢ e


Latex:


Latex:
\mforall{}g:IAbMonoid.  \mforall{}a:|g|.    (g-unit(a)  \mLeftarrow{}{}\mRightarrow{}  a  \msim{}  e)


By


Latex:
((Unfold  `munit`  0  THEN  GenRepD  )  THENA  Auto)




Home Index