1. g : IMonoid
⊢ Ident(|g|;*;e)
{ D 1 }
1. g : GrpSig
2. IsMonoid(|g|;*;e)