Step * of Lemma mon_nat_op_one

[g:IMonoid]. ∀[e:|g|].  ((1 ⋅ e) e ∈ |g|)
BY
((UnivCD) THENA Auto) }

1
1. IMonoid
2. |g|
⊢ (1 ⋅ e) e ∈ |g|


Latex:


Latex:
\mforall{}[g:IMonoid].  \mforall{}[e:|g|].    ((1  \mcdot{}  e)  =  e)


By


Latex:
((UnivCD)  THENA  Auto)




Home Index