let A, B be AbGroup; :: thesis:
let f be Homomorphism of A,B; :: thesis:
assume A1: ( f is one-to-one & ([#] B) \ (rng f) <> {} ) ; :: thesis:
A2: dom f = [#] A by FUNCT_2:def 1;
consider X being non empty set such that
A3: ( ([#] A) /\ X = {} & ex h being Function st
( h is one-to-one & dom h = ([#] B) \ (rng f) & rng h = X ) ) by A1, Th2;
consider h being Function such that
A4: ( h is one-to-one & dom h = ([#] B) \ (rng f) & rng h = X & ([#] A) /\ X = {} ) by A3;
defpred S₁[ Element of B, Element of ([#] A) \/ X] means ( ( $1 in rng f & (f ") . $1 = $2 ) or ( not $1 in rng f & $2 = h . $1 ) );
set C1 = ([#] A) \/ X;

A5: now :: thesis:

let y be Element of B; :: thesis:

per cases ;

suppose A6: y in rng f ; :: thesis:

then consider x being object such that
A7: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
(f ") . y = x by A7, A1, FUNCT_1:34;
then (f ") . y in ([#] A) \/ X by A7, XBOOLE_0:def 3;
hence ex x being Element of ([#] A) \/ X st S₁[y,x] by A6; :: thesis:

end;

suppose A8: not y in rng f ; :: thesis:

then y in dom h by A4, XBOOLE_0:def 5;
then h . y in X by A4, FUNCT_1:def 3;
then h . y in ([#] A) \/ X by XBOOLE_0:def 3;
hence ex x being Element of ([#] A) \/ X st S₁[y,x] by A8; :: thesis:

end;

consider g being Function of the carrier of B,(([#] A) \/ X) such that
A10: for x being Element of B holds S₁[x,g . x] from FUNCT_2:sch 3(A5);
A11: ( dom g = the carrier of B & rng g c= ([#] A) \/ X ) by FUNCT_2:def 1;
A12: g is bijective

proof

for o being object st o in ([#] A) \/ X holds
o in rng g

proof

let o be object ; :: thesis:
assume A13: o in ([#] A) \/ X ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A14: o in [#] A ; :: thesis:

then A15: o in dom f by FUNCT_2:def 1;
f . o in [#] B by A14, FUNCT_2:5;
then consider b being Element of B such that
A16: b = f . o ;
reconsider x = o as Element of ([#] A) \/ X by A13;
S₁[b,x] by A16, A1, A15, FUNCT_1:3, FUNCT_1:34;
then g . b = x by A10;
hence o in rng g by A11, FUNCT_1:3; :: thesis:

end;

suppose o in X ; :: thesis:

then consider x being object such that
A18: ( x in dom h & o = h . x ) by A4, FUNCT_1:def 3;
reconsider c = o as Element of ([#] A) \/ X by A13;
reconsider b = x as Element of B by A4, A18;
S₁[b,c] by A18, A4, XBOOLE_0:def 5;
then g . b = c by A10;
hence o in rng g by A11, FUNCT_1:3; :: thesis:

end;

then ([#] A) \/ X c= rng g ;
then A19: ([#] A) \/ X = rng g ;
reconsider g = g as ([#] A) \/ X -valued Function ;
A20: g is onto by A19;
for o1, o2 being object st o1 in dom g & o2 in dom g & g . o1 = g . o2 holds
o1 = o2

proof

let o1, o2 be object ; :: thesis:
assume A21: ( o1 in dom g & o2 in dom g ) ; :: thesis:
assume A22: g . o1 = g . o2 ; :: thesis:
assume A23: o1 <> o2 ; :: thesis:

per cases ;

suppose A24: ( o1 in rng f & o2 in rng f ) ; :: thesis:

then consider x1 being object such that
A25: ( x1 in dom f & o1 = f . x1 ) by FUNCT_1:def 3;
reconsider c1 = x1 as Element of ([#] A) \/ X by A25, XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by A25, FUNCT_2:5;
A26: (f ") . b1 = c1 by A1, A25, FUNCT_1:34;
S₁[b1,c1] by A24, A1, A25, FUNCT_1:34;
then A27: g . b1 = c1 by A10;
consider x2 being object such that
A28: ( x2 in dom f & o2 = f . x2 ) by A24, FUNCT_1:def 3;
reconsider c2 = x2 as Element of ([#] A) \/ X by A28, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by A28, FUNCT_2:5;
A29: (f ") . b2 = c2 by A1, A28, FUNCT_1:34;
S₁[b2,c2] by A24, A1, A28, FUNCT_1:34;
then A30: g . b2 = c2 by A10;
A31: ( b1 in dom (f ") & b2 in dom (f ") ) by A24, A1, FUNCT_1:33;
f " is one-to-one by A1;
hence contradiction by A22, A27, A30, A26, A29, A23, A31; :: thesis:

end;

suppose A33: ( o1 in rng f & not o2 in rng f ) ; :: thesis:

then consider x1 being object such that
A34: ( x1 in dom f & o1 = f . x1 ) by FUNCT_1:def 3;
reconsider c1 = x1 as Element of ([#] A) \/ X by A34, XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by A34, FUNCT_2:5;
A35: S₁[b1,c1] by A33, A1, A34, FUNCT_1:34;
o2 in [#] B by FUNCT_2:def 1, A21;
then o2 in dom h by A4, A33, XBOOLE_0:def 5;
then h . o2 in X by A4, FUNCT_1:def 3;
then consider x2 being Element of X such that
A37: x2 = h . o2 ;
reconsider c2 = x2 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by FUNCT_2:def 1, A21;
g . b2 = c2 by A10, A37, A33;
then c1 = c2 by A10, A35, A22;
hence contradiction by A4, A34, XBOOLE_0:def 4; :: thesis:

end;

suppose A40: ( not o1 in rng f & o2 in rng f ) ; :: thesis:

then consider x2 being object such that
A41: ( x2 in dom f & o2 = f . x2 ) by FUNCT_1:def 3;
reconsider c2 = x2 as Element of ([#] A) \/ X by A41, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B by A41, FUNCT_2:5;
A42: S₁[b2,c2] by A40, A1, A41, FUNCT_1:34;
A43: o1 in [#] B by FUNCT_2:def 1, A21;
o1 in dom h by A4, A40, XBOOLE_0:def 5, A43;
then h . o1 in X by A4, FUNCT_1:def 3;
then consider x1 being Element of X such that
A44: x1 = h . o1 ;
reconsider c1 = x1 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B by FUNCT_2:def 1, A21;
A45: g . b1 = c1 by A44, A40, A10;
c1 = c2 by A45, A10, A42, A22;
hence contradiction by A4, A41, XBOOLE_0:def 4; :: thesis:

end;

suppose A47: ( not o1 in rng f & not o2 in rng f ) ; :: thesis:

o1 in [#] B by FUNCT_2:def 1, A21;
then A48: o1 in dom h by A4, A47, XBOOLE_0:def 5;
reconsider b1 = o1 as Element of B by FUNCT_2:def 1, A21;
o2 in [#] B by A21, FUNCT_2:def 1;
then A50: o2 in dom h by A4, A47, XBOOLE_0:def 5;
reconsider b2 = o2 as Element of B by A21, FUNCT_2:def 1;
h . o1 = g . b1 by A10, A47
.= g . b2 by A22
.= h . o2 by A10, A47 ;
hence contradiction by A48, A50, A23, A4; :: thesis:

end;

then g is one-to-one ;
hence g is bijective by A20; :: thesis:

end;

reconsider C = emb_AbGr g as AbGroup by A12, Th12;
A52: [#] C = ([#] A) \/ X ;
reconsider G = g as Function of B,C ;
G is additive

proof

for o1, o2 being Element of B holds G . (o1 + o2) = (G . o1) + (G . o2)

proof

let o1, o2 be Element of B; :: thesis:

per cases ;

suppose A53: ( o1 in rng f & o2 in rng f ) ; :: thesis:

then consider x1 being object such that
A54: ( x1 in dom f & o1 = f . x1 ) by FUNCT_1:def 3;
reconsider c1 = x1 as Element of ([#] A) \/ X by A54, XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B ;
A55: S₁[b1,c1] by A53, A1, A54, FUNCT_1:34;
consider x2 being object such that
A56: ( x2 in dom f & o2 = f . x2 ) by A53, FUNCT_1:def 3;
reconsider c2 = x2 as Element of ([#] A) \/ X by A56, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B ;
A57: S₁[b2,c2] by A53, A1, A56, FUNCT_1:34;
reconsider x1 = x1, x2 = x2 as Element of ([#] A) \/ X by A56, A54, XBOOLE_0:def 3;
A58: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A55 ;
A59: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A57 ;
A60: G . o1 = x1 by A10, A55;
G . o2 = x2 by A10, A57;
then (G . o1) + (G . o2) = addemb (g,x1,x2) by Def9, A60
.= g . (o1 + o2) by A58, A59, A12, Def8 ;
hence G . (o1 + o2) = (G . o1) + (G . o2) ; :: thesis:

end;

suppose A62: ( o1 in rng f & not o2 in rng f ) ; :: thesis:

then consider x1 being object such that
A63: ( x1 in dom f & o1 = f . x1 ) by FUNCT_1:def 3;
reconsider c1 = x1 as Element of ([#] A) \/ X by XBOOLE_0:def 3, A63;
reconsider b1 = o1 as Element of B ;
A64: S₁[b1,c1] by A62, A1, A63, FUNCT_1:34;
o2 in dom h by A4, A62, XBOOLE_0:def 5;
then h . o2 in X by A4, FUNCT_1:def 3;
then consider x2 being Element of X such that
A65: x2 = h . o2 ;
reconsider c2 = x2 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B ;
reconsider x1 = x1, x2 = x2 as Element of ([#] A) \/ X by A63, XBOOLE_0:def 3;
A66: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A64 ;
A67: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A65, A62 ;
A68: G . o1 = x1 by A10, A64;
G . o2 = x2 by A10, A65, A62;
then (G . o1) + (G . o2) = addemb (g,x1,x2) by Def9, A68
.= g . (o1 + o2) by A66, A67, A12, Def8 ;
hence G . (o1 + o2) = (G . o1) + (G . o2) ; :: thesis:

end;

suppose A70: ( not o1 in rng f & o2 in rng f ) ; :: thesis:

then o1 in dom h by A4, XBOOLE_0:def 5;
then h . o1 in X by A4, FUNCT_1:def 3;
then consider x1 being Element of X such that
A71: x1 = h . o1 ;
reconsider c1 = x1 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B ;
consider x2 being object such that
A72: ( x2 in dom f & o2 = f . x2 ) by A70, FUNCT_1:def 3;
reconsider c2 = x2 as Element of ([#] A) \/ X by A72, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B ;
A73: S₁[b2,c2] by A70, A1, A72, FUNCT_1:34;
reconsider x1 = x1, x2 = x2 as Element of ([#] A) \/ X by A72, XBOOLE_0:def 3;
A74: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A71, A70 ;
A75: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A73 ;
A76: G . o2 = x2 by A10, A73;
G . o1 = x1 by A10, A71, A70;
then (G . o1) + (G . o2) = addemb (g,x1,x2) by Def9, A76
.= g . (o1 + o2) by A75, A74, A12, Def8 ;
hence G . (o1 + o2) = (G . o1) + (G . o2) ; :: thesis:

end;

suppose A78: ( not o1 in rng f & not o2 in rng f ) ; :: thesis:

then o1 in dom h by A4, XBOOLE_0:def 5;
then h . o1 in X by A4, FUNCT_1:def 3;
then consider x1 being Element of X such that
A79: x1 = h . o1 ;
reconsider c1 = x1 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
reconsider b1 = o1 as Element of B ;
o2 in dom h by A4, A78, XBOOLE_0:def 5;
then h . o2 in X by A4, FUNCT_1:def 3;
then consider x2 being Element of X such that
A80: x2 = h . o2 ;
reconsider c2 = x2 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B ;
reconsider x1 = x1, x2 = x2 as Element of ([#] A) \/ X by XBOOLE_0:def 3;
A81: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A79, A78 ;
A82: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A80, A78 ;
A83: G . o1 = x1 by A10, A79, A78;
A84: G . o2 = x2 by A10, A80, A78;
(G . o1) + (G . o2) = addemb (g,x1,x2) by Def9, A83, A84
.= g . (o1 + o2) by A82, A81, A12, Def8 ;
hence G . (o1 + o2) = (G . o1) + (G . o2) ; :: thesis:

end;

hence G is additive ; :: thesis:

end;

then reconsider G = G as Homomorphism of B,C ;
A85: for o being object st o in [#] A holds
(G * f) . o = o

proof

let o be object ; :: thesis:
assume A86: o in [#] A ; :: thesis:
then A87: f . o in rng f by A2, FUNCT_1:3;
reconsider c1 = o as Element of ([#] A) \/ X by A86, XBOOLE_0:def 3;
reconsider b1 = f . o as Element of B by A87;
A88: S₁[b1,c1] by A86, A2, FUNCT_1:3, A1, FUNCT_1:34;
(G * f) . o = G . b1 by A2, A86, FUNCT_1:13
.= c1 by A10, A88 ;
hence (G * f) . o = o ; :: thesis:

end;

A89: rng (id ([#] A)) c= ([#] A) \/ X by XBOOLE_1:7;
reconsider i = id A as Function of (dom (id A)),C by A89, FUNCT_2:2;
i is Function of A,C ;
then reconsider i = id A as Function of A,C ;
A90: G * f = i by A85;
A91: G * f is Homomorphism of A,C by GROUP_14:6;
A is SubAbGr of C by Th13, A90, A91;
hence ex C being AbGroup ex X being set ex h being Function ex G being Function of B,C st
( X /\ ([#] A) = {} & h is one-to-one & dom h = ([#] B) \ (rng f) & rng h = X & [#] C = X \/ ([#] A) & A is SubAbGr of C & G is Homomorphism of B,C & id A = G * f ) by A4, A52, A90; :: thesis: