Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frgpup.b | |
|
frgpup.n | |
||
frgpup.t | |
||
frgpup.h | |
||
frgpup.i | |
||
frgpup.a | |
||
frgpup.w | |
||
frgpup.r | |
||
frgpup.g | |
||
frgpup.x | |
||
frgpup.e | |
||
Assertion | frgpup1 | |