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

proof

let x, y1, y2 be object ; :: thesis: ( [x,y1] in ((nat_hom R) ~) * f & [x,y2] in ((nat_hom R) ~) * f implies y1 = y2 )
assume [x,y1] in ((nat_hom R) ~) * f ; :: thesis: ( not [x,y2] in ((nat_hom R) ~) * f or y1 = y2 )
then consider z1 being object 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: y1 = y2
then consider z2 being object 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 ( z1 in dom (nat_hom R) & z2 in dom (nat_hom R) ) by XTUPLE_0:def 12;
then reconsider z1 = z1, z2 = z2 as Element of M ;
A7: ( x = (nat_hom R) . z1 & x = (nat_hom R) . z2 ) by A6, FUNCT_1:1;
A8: ( f . z1 = y1 & f . z2 = y2 ) by A4, A5, FUNCT_1:1;
( (nat_hom R) . z1 = Class (R,z1) & (nat_hom R) . z2 = Class (R,z2) ) by Def6;
then z2 in Class (R,z1) by A7, EQREL_1:23;
then [z1,z2] in equ_kernel f by A3, EQREL_1:18;
hence y1 = y2 by A8, Def8; :: thesis: verum

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 A9: dom ((nat_hom R) ~) = the carrier of (M ./. R) by RELAT_1:20;
the carrier of M c= dom f by FUNCT_2:def 1;
then dom (nat_hom R) c= dom f ;
then rng ((nat_hom R) ~) c= dom f by RELAT_1:20;
then A10: dom g = the carrier of (M ./. R) by A9, RELAT_1:27;
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:20;
then A11: rng g = the carrier of H by A2, RELAT_1:28;
then reconsider g = g as Function of (M ./. R),H by A10, FUNCT_2:1;
take g ; :: thesis: ( f = g * (nat_hom R) & g is bijective & g is multiplicative )
for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume A12: x1 in dom g ; :: thesis: ( not x2 in dom g or not g . x1 = g . x2 or x1 = x2 )
assume A13: x2 in dom g ; :: thesis: ( not g . x1 = g . x2 or x1 = x2 )
assume A14: g . x1 = g . x2 ; :: thesis: x1 = x2
set y = g . x1;
[x1,(g . x1)] in g by A12, FUNCT_1:1;
then consider z1 being object such that
A15: ( [x1,z1] in (nat_hom R) ~ & [z1,(g . x1)] in f ) by RELAT_1:def 8;
[x2,(g . x1)] in g by A14, A13, FUNCT_1:1;
then consider z2 being object such that
A16: ( [x2,z2] in (nat_hom R) ~ & [z2,(g . x1)] in f ) by RELAT_1:def 8;
A17: ( [z1,x1] in nat_hom R & [z2,x2] in nat_hom R ) by A15, A16, RELAT_1:def 7;
then ( z1 in dom (nat_hom R) & z2 in dom (nat_hom R) ) by XTUPLE_0:def 12;
then reconsider z1 = z1, z2 = z2 as Element of M ;
( z1 in dom f & z2 in dom f & f . z1 = g . x1 & f . z2 = g . x1 ) by A15, A16, FUNCT_1:1;
then [z1,z2] in equ_kernel f by Def8;
then A18: z2 in Class (R,z1) by A3, EQREL_1:18;
A19: ( (nat_hom R) . z1 = Class (R,z1) & (nat_hom R) . z2 = Class (R,z2) ) by Def6;
( x1 = (nat_hom R) . z1 & x2 = (nat_hom R) . z2 ) by A17, FUNCT_1:1;
hence x1 = x2 by A19, A18, EQREL_1:23; :: thesis: verum

end;

then A20: g is one-to-one by FUNCT_1:def 4;
A21: for x being object holds
( x in dom f iff ( x in dom (nat_hom R) & (nat_hom R) . x in dom g ) )

proof

let x be object ; :: thesis: ( x in dom f iff ( x in dom (nat_hom R) & (nat_hom R) . x in dom g ) )

hereby :: thesis: ( x in dom (nat_hom R) & (nat_hom R) . x in dom g implies x in dom f )

assume x in dom f ; :: thesis: ( x in dom (nat_hom R) & (nat_hom R) . x in dom g )
then x in the carrier of M ;
hence x in dom (nat_hom R) by FUNCT_2:def 1; :: thesis: (nat_hom R) . x in dom g
then (nat_hom R) . x in rng (nat_hom R) by FUNCT_1:3;
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: verum

end;

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

end;

for x being object st x in dom f holds
f . x = g . ((nat_hom R) . x)

proof

let x be object ; :: thesis: ( x in dom f implies f . x = g . ((nat_hom R) . x) )
assume A22: x in dom f ; :: thesis: f . x = g . ((nat_hom R) . x)
set y = (nat_hom R) . x;
(nat_hom R) . x in dom g by A22, A21;
then [((nat_hom R) . x),(g . ((nat_hom R) . x))] in g by FUNCT_1:1;
then consider z being object such that
A23: ( [((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 A23, RELAT_1:def 7;
then A24: ( z in dom (nat_hom R) & (nat_hom R) . x = (nat_hom R) . z ) by FUNCT_1:1;
A25: ( z in dom f & g . ((nat_hom R) . x) = f . z ) by A23, FUNCT_1:1;
then reconsider z9 = z, x9 = x as Element of M by A22;
( (nat_hom R) . z9 = Class (R,z9) & (nat_hom R) . x9 = Class (R,x9) ) by Def6;
then z9 in Class (R,x9) by A24, EQREL_1:23;
then [x,z] in R by EQREL_1:18;
hence f . x = g . ((nat_hom R) . x) by A25, A3, Def8; :: thesis: verum

end;

hence f = g * (nat_hom R) by A21, FUNCT_1:10; :: thesis: ( g is bijective & g is multiplicative )
g is onto by A11, FUNCT_2:def 3;
hence g is bijective by A20; :: thesis: g is multiplicative
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: g . (v * w) = (g . v) * (g . w)
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:1;
then consider z being object such that
A26: ( [(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 A26, RELAT_1:def 7;
then A27: ( z in dom (nat_hom R) & (nat_hom R) . z = v * w ) by FUNCT_1:1;
A28: f . z = g . (v * w) by A26, FUNCT_1:1;
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:1;
then consider z1 being object such that
A29: ( [v,z1] in (nat_hom R) ~ & [z1,(g . v)] in f ) by RELAT_1:def 8;
[z1,v] in nat_hom R by A29, RELAT_1:def 7;
then A30: ( z1 in dom (nat_hom R) & (nat_hom R) . z1 = v ) by FUNCT_1:1;
A31: f . z1 = g . v by A29, FUNCT_1:1;
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:1;
then consider z2 being object such that
A32: ( [w,z2] in (nat_hom R) ~ & [z2,(g . w)] in f ) by RELAT_1:def 8;
[z2,w] in nat_hom R by A32, RELAT_1:def 7;
then A33: ( z2 in dom (nat_hom R) & (nat_hom R) . z2 = w ) by FUNCT_1:1;
A34: f . z2 = g . w by A32, FUNCT_1:1;
reconsider z1 = z1, z2 = z2, z = z as Element of M by A30, A33, A27;
A35: (nat_hom R) . z = (nat_hom R) . (z1 * z2) by A30, A33, A27, GROUP_6:def 6;
( (nat_hom R) . (z1 * z2) = Class (R,(z1 * z2)) & (nat_hom R) . z = Class (R,z) ) by Def6;
then z1 * z2 in Class (R,z) by A35, EQREL_1:23;
then [z,(z1 * z2)] in R by EQREL_1:18;
then A36: f . z = f . (z1 * z2) by A3, Def8
.= (f . z1) * (f . z2) by A1, GROUP_6:def 6 ;
A37: [(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 A31, A34, A36, A28, BINOP_1:def 1
.= ( the multF of N | [: the carrier of H, the carrier of H:]) . [(g . v),(g . w)] by A37, FUNCT_1:49
.= ( 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 2
.= (g . v) * (g . w) by Def9 ; :: thesis: verum

end;

hence g is multiplicative by GROUP_6:def 6; :: thesis: verum