let M, N be non empty multMagma ; :: thesis: for R being compatible Equivalence_Relation of M
for g1, g2 being Function of (M ./. R),N st g1 * (nat_hom R) = g2 * (nat_hom R) holds
g1 = g2
let R be compatible Equivalence_Relation of M; :: thesis: for g1, g2 being Function of (M ./. R),N st g1 * (nat_hom R) = g2 * (nat_hom R) holds
g1 = g2
let g1, g2 be Function of (M ./. R),N; :: thesis: ( g1 * (nat_hom R) = g2 * (nat_hom R) implies g1 = g2 )
assume A1: g1 * (nat_hom R) = g2 * (nat_hom R) ; :: thesis: g1 = g2
set Y = rng (nat_hom R);
rng (nat_hom R) = the carrier of (M ./. R) by FUNCT_2:def 3;
then ( dom g1 = rng (nat_hom R) & dom g2 = rng (nat_hom R) ) by FUNCT_2:def 1;
hence g1 = g2 by A1, FUNCT_1:86; :: thesis: verum