theorem :: ALGSTR_4:37

for X being non empty set
for R being compatible Equivalence_Relation of (free_magma X) holds (free_magma X) ./. R = the_submagma_generated_by ((nat_hom R) .: ((canon_image (X,1)) .: X))