Step
*
of Lemma
munit_of_op
∀g:IAbMonoid. ∀a,b:|g|.  ((g-unit(a * b)) 
⇒ ((g-unit(a)) ∧ (g-unit(b))))
BY
{ ((GenUnivCD) THENA Auto) }
1
1. g : IAbMonoid
2. a : |g|
3. b : |g|
4. g-unit(a * b)
⊢ g-unit(a)
2
1. g : IAbMonoid
2. a : |g|
3. b : |g|
4. g-unit(a * b)
⊢ g-unit(b)
Latex:
Latex:
\mforall{}g:IAbMonoid.  \mforall{}a,b:|g|.    ((g-unit(a  *  b))  {}\mRightarrow{}  ((g-unit(a))  \mwedge{}  (g-unit(b))))
By
Latex:
((GenUnivCD)  THENA  Auto)
Home
Index