Description: The image of a monoid G under a monoid homomorphism F is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ghmgrp.f | |
|
ghmgrp.x | |
||
ghmgrp.y | |
||
ghmgrp.p | |
||
ghmgrp.q | |
||
ghmgrp.1 | |
||
mhmmnd.3 | |
||
Assertion | mhmmnd | |