Step * of Lemma mon_nat_op_id

[g:IMonoid]. ∀[n:ℕ].  ((n ⋅ e) e ∈ |g|)
BY
((D THENM 0) THENA Auto) }

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


Latex:


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


By


Latex:
((D  0  THENM  D  0)  THENA  Auto)




Home Index