let N, M be non empty multMagma ; :: thesis:
let f be Function of M,N; :: thesis:
let H be non empty multSubmagma of N; :: thesis:
let R be compatible Equivalence_Relation of M; :: thesis:
assume A1: f is multiplicative ; :: thesis:
assume A2: the carrier of H = rng f ; :: thesis:
assume A3: R = equ_kernel f ; :: thesis:
set g = ((nat_hom R) ~ ) * f;
for x, y1, y2 being set st [x,y1] in ((nat_hom R) ~ ) * f & [x,y2] in ((nat_hom R) ~ ) * f holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis:
assume [x,y1] in ((nat_hom R) ~ ) * f ; :: thesis:
then consider z1 being set such that
A4: ( [x,z1] in (nat_hom R) ~ & [z1,y1] in f ) by RELAT_1:def 8;
assume [x,y2] in ((nat_hom R) ~ ) * f ; :: thesis:
then consider z2 being set such that
A5: ( [x,z2] in (nat_hom R) ~ & [z2,y2] in f ) by RELAT_1:def 8;
A6: ( [z1,x] in nat_hom R & [z2,x] in nat_hom R ) by A4, A5, RELAT_1:def 7;
then A7: ( z1 in dom (nat_hom R) & z2 in dom (nat_hom R) ) by RELAT_1:def 4;
reconsider z1 = z1, z2 = z2 as Element of M by A7;
A8: ( x = (nat_hom R) . z1 & x = (nat_hom R) . z2 ) by A6, FUNCT_1:8;
A9: ( f . z1 = y1 & f . z2 = y2 ) by A4, A5, FUNCT_1:8;
( (nat_hom R) . z1 = Class R,z1 & (nat_hom R) . z2 = Class R,z2 ) by Def7;
then z2 in Class R,z1 by A8, EQREL_1:31;
then [z1,z2] in equ_kernel f by A3, EQREL_1:26;
hence y1 = y2 by A9, Def9; :: thesis:

end;

then reconsider g = ((nat_hom R) ~ ) * f as Function by FUNCT_1:def 1;
rng (nat_hom R) = the carrier of (M ./. R) by FUNCT_2:def 3;
then A10: dom ((nat_hom R) ~ ) = the carrier of (M ./. R) by RELAT_1:37;
the carrier of M c= dom f by FUNCT_2:def 1;
then dom (nat_hom R) c= dom f by FUNCT_2:def 1;
then rng ((nat_hom R) ~ ) c= dom f by RELAT_1:37;
then A11: dom g = the carrier of (M ./. R) by A10, RELAT_1:46;
dom f c= the carrier of M ;
then dom f c= dom (nat_hom R) by FUNCT_2:def 1;
then dom f c= rng ((nat_hom R) ~ ) by RELAT_1:37;
then A12: rng g = the carrier of H by A2, RELAT_1:47;
reconsider g = g as Function of (M ./. R),H by A11, A12, FUNCT_2:3;
take g ; :: thesis:
for x1, x2 being set st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume A13: x1 in dom g ; :: thesis:
assume A14: x2 in dom g ; :: thesis:
assume A15: g . x1 = g . x2 ; :: thesis:
set y = g . x1;
[x1,(g . x1)] in g by A13, FUNCT_1:8;
then consider z1 being set such that
A16: ( [x1,z1] in (nat_hom R) ~ & [z1,(g . x1)] in f ) by RELAT_1:def 8;
[x2,(g . x1)] in g by A15, A14, FUNCT_1:8;
then consider z2 being set such that
A17: ( [x2,z2] in (nat_hom R) ~ & [z2,(g . x1)] in f ) by RELAT_1:def 8;
A18: ( [z1,x1] in nat_hom R & [z2,x2] in nat_hom R ) by A16, A17, RELAT_1:def 7;
then A19: ( z1 in dom (nat_hom R) & z2 in dom (nat_hom R) ) by RELAT_1:def 4;
reconsider z1 = z1, z2 = z2 as Element of M by A19;
( z1 in dom f & z2 in dom f & f . z1 = g . x1 & f . z2 = g . x1 ) by A16, A17, FUNCT_1:8;
then [z1,z2] in equ_kernel f by Def9;
then A20: z2 in Class R,z1 by A3, EQREL_1:26;
A21: ( (nat_hom R) . z1 = Class R,z1 & (nat_hom R) . z2 = Class R,z2 ) by Def7;
( x1 = (nat_hom R) . z1 & x2 = (nat_hom R) . z2 ) by A18, FUNCT_1:8;
hence x1 = x2 by A21, A20, EQREL_1:31; :: thesis:

end;

then A22: g is one-to-one by FUNCT_1:def 8;
A23: for x being set holds
( x in dom f iff ( x in dom (nat_hom R) & (nat_hom R) . x in dom g ) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in dom f ; :: thesis:
then x in the carrier of M ;
hence x in dom (nat_hom R) by FUNCT_2:def 1; :: thesis:
then (nat_hom R) . x in rng (nat_hom R) by FUNCT_1:12;
then (nat_hom R) . x in the carrier of (M ./. R) ;
hence (nat_hom R) . x in dom g by FUNCT_2:def 1; :: thesis:

end;

assume ( x in dom (nat_hom R) & (nat_hom R) . x in dom g ) ; :: thesis:
then x in the carrier of M ;
hence x in dom f by FUNCT_2:def 1; :: thesis:

end;

A24: for x being set st x in dom f holds
f . x = g . ((nat_hom R) . x)

proof

let x be set ; :: thesis:
assume A25: x in dom f ; :: thesis:
set y = (nat_hom R) . x;
(nat_hom R) . x in dom g by A25, A23;
then [((nat_hom R) . x),(g . ((nat_hom R) . x))] in g by FUNCT_1:8;
then consider z being set such that
A26: ( [((nat_hom R) . x),z] in (nat_hom R) ~ & [z,(g . ((nat_hom R) . x))] in f ) by RELAT_1:def 8;
[z,((nat_hom R) . x)] in nat_hom R by A26, RELAT_1:def 7;
then A27: ( z in dom (nat_hom R) & (nat_hom R) . x = (nat_hom R) . z ) by FUNCT_1:8;
A28: ( z in dom f & g . ((nat_hom R) . x) = f . z ) by A26, FUNCT_1:8;
then reconsider z9 = z, x9 = x as Element of M by A25;
( (nat_hom R) . z9 = Class R,z9 & (nat_hom R) . x9 = Class R,x9 ) by Def7;
then z9 in Class R,x9 by A27, EQREL_1:31;
then [x,z] in R by EQREL_1:26;
hence f . x = g . ((nat_hom R) . x) by A28, A3, Def9; :: thesis:

end;

thus f = g * (nat_hom R) by A23, A24, FUNCT_1:20; :: thesis:
g is onto by A12, FUNCT_2:def 3;
hence g is bijective by A22; :: thesis:
for v, w being Element of (M ./. R) holds g . (v * w) = (g . v) * (g . w)

proof

let v, w be Element of (M ./. R); :: thesis:
v * w in the carrier of (M ./. R) ;
then v * w in dom g by FUNCT_2:def 1;
then [(v * w),(g . (v * w))] in g by FUNCT_1:8;
then consider z being set such that
A29: ( [(v * w),z] in (nat_hom R) ~ & [z,(g . (v * w))] in f ) by RELAT_1:def 8;
[z,(v * w)] in nat_hom R by A29, RELAT_1:def 7;
then A30: ( z in dom (nat_hom R) & (nat_hom R) . z = v * w ) by FUNCT_1:8;
A31: f . z = g . (v * w) by A29, FUNCT_1:8;
v in the carrier of (M ./. R) ;
then v in dom g by FUNCT_2:def 1;
then [v,(g . v)] in g by FUNCT_1:8;
then consider z1 being set such that
A32: ( [v,z1] in (nat_hom R) ~ & [z1,(g . v)] in f ) by RELAT_1:def 8;
[z1,v] in nat_hom R by A32, RELAT_1:def 7;
then A33: ( z1 in dom (nat_hom R) & (nat_hom R) . z1 = v ) by FUNCT_1:8;
A34: f . z1 = g . v by A32, FUNCT_1:8;
w in the carrier of (M ./. R) ;
then w in dom g by FUNCT_2:def 1;
then [w,(g . w)] in g by FUNCT_1:8;
then consider z2 being set such that
A35: ( [w,z2] in (nat_hom R) ~ & [z2,(g . w)] in f ) by RELAT_1:def 8;
[z2,w] in nat_hom R by A35, RELAT_1:def 7;
then A36: ( z2 in dom (nat_hom R) & (nat_hom R) . z2 = w ) by FUNCT_1:8;
A37: f . z2 = g . w by A35, FUNCT_1:8;
reconsider z1 = z1, z2 = z2, z = z as Element of M by A33, A36, A30;
A38: (nat_hom R) . z = (nat_hom R) . (z1 * z2) by A33, A36, A30, GROUP_6:def 7;
( (nat_hom R) . (z1 * z2) = Class R,(z1 * z2) & (nat_hom R) . z = Class R,z ) by Def7;
then z1 * z2 in Class R,z by A38, EQREL_1:31;
then [z,(z1 * z2)] in R by EQREL_1:26;
then A39: f . z = f . (z1 * z2) by A3, Def9
.= (f . z1) * (f . z2) by A1, GROUP_6:def 7 ;
A40: [(g . v),(g . w)] in [:the carrier of H,the carrier of H:] by ZFMISC_1:def 2;
thus g . (v * w) = the multF of N . [(g . v),(g . w)] by A34, A37, A39, A31, BINOP_1:def 1
.= (the multF of N | [:the carrier of H,the carrier of H:]) . [(g . v),(g . w)] by A40, FUNCT_1:72
.= (the multF of N | [:the carrier of H,the carrier of H:]) . (g . v),(g . w) by BINOP_1:def 1
.= (the multF of N || the carrier of H) . (g . v),(g . w) by REALSET1:def 3
.= (g . v) * (g . w) by Def10 ; :: thesis:

end;

hence g is multiplicative by GROUP_6:def 7; :: thesis: