let X be non empty set ; :: thesis: 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))
let R be compatible Equivalence_Relation of (free_magma X); :: thesis: (free_magma X) ./. R = the_submagma_generated_by ((nat_hom R) .: ((canon_image (X,1)) .: X))
set A = (canon_image (X,1)) .: X;
reconsider A = (canon_image (X,1)) .: X as Subset of (free_magma X) ;
A1: the carrier of (the_submagma_generated_by A) = the carrier of (free_magma X) by Th36;
the carrier of ((free_magma X) ./. R) = rng (nat_hom R) by FUNCT_2:def 3;
then the carrier of ((free_magma X) ./. R) = (nat_hom R) .: (dom (nat_hom R)) by RELAT_1:113;
then the carrier of ((free_magma X) ./. R) = (nat_hom R) .: the carrier of (the_submagma_generated_by A) by A1, FUNCT_2:def 1;
then the carrier of ((free_magma X) ./. R) = the carrier of (the_submagma_generated_by ((nat_hom R) .: A)) by Th15;
hence (free_magma X) ./. R = the_submagma_generated_by ((nat_hom R) .: ((canon_image (X,1)) .: X)) by Th7; :: thesis: verum