Step
*
1
1
of Lemma
mon_ident
1. g : GrpSig
2. IsMonoid(|g|;*;e)
⊢ Ident(|g|;*;e)
BY
{ D 2 THEN Trivial }
Latex:
Latex:
1. g : GrpSig
2. IsMonoid(|g|;*;e)
\mvdash{} Ident(|g|;*;e)
By
Latex:
D 2 THEN Trivial
Home
Index