Description: The structure with the singleton containing only the identity function
restricted to a set A as base set and the function composition as
group operation, constructed by (structure) restricting the monoid of
endofunctions on A to that singleton, is a monoid whose base set is
a subset of the base set of the monoid of endofunctions on A .
(Contributed by AV, 17-Feb-2024)
Ref
Expression
Hypotheses
idressubmefmnd.g
No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-