let A, B be Ring; :: thesis:
let f be Function of A,B; :: thesis:
assume A1: ( f is monomorphism & ([#] 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

([#] A) \/ X c= rng g

proof

let o be object ; :: according to TARSKI:def 3 :: 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;
A36: o2 in [#] B by FUNCT_2:def 1, A21;
o2 in dom h by A36, 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;
g . b1 = c1 by A44, A40, A10;
then c1 = c2 by 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_Ring g as Ring by A12, Th6;
A52: [#] C = ([#] A) \/ X ;
reconsider G = g as Function of B,C ;
A53: G is linear

proof

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

proof

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

per cases ;

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

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

end;

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

then consider x1 being object such that
A65: ( 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, A65;
reconsider b1 = o1 as Element of B ;
A66: S₁[b1,c1] by A64, A1, A65, FUNCT_1:34;
o2 in dom h by A4, A64, XBOOLE_0:def 5;
then h . o2 in X by A4, FUNCT_1:def 3;
then consider x2 being Element of X such that
A67: 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 A65, XBOOLE_0:def 3;
A68: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A66 ;
A69: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A67, A64 ;
A70: G . o1 = x1 by A10, A66;
A71: G . o2 = x2 by A10, A67, A64;
then A72: (G . o1) + (G . o2) = addemb (g,x1,x2) by Def2, A70
.= g . (o1 + o2) by A68, A69, A12, Def1 ;
(G . o1) * (G . o2) = multemb (g,x1,x2) by Def4, A70, A71
.= g . (o1 * o2) by A68, A69, A12, Def3 ;
hence ( G . (o1 + o2) = (G . o1) + (G . o2) & G . (o1 * o2) = (G . o1) * (G . o2) ) by A72; :: thesis:

end;

suppose A73: ( 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
A74: 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
A75: ( x2 in dom f & o2 = f . x2 ) by A73, FUNCT_1:def 3;
reconsider c2 = x2 as Element of ([#] A) \/ X by A75, XBOOLE_0:def 3;
reconsider b2 = o2 as Element of B ;
A76: S₁[b2,c2] by A73, A1, A75, FUNCT_1:34;
reconsider x1 = x1, x2 = x2 as Element of ([#] A) \/ X by A75, XBOOLE_0:def 3;
A77: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A74, A73 ;
A78: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A76 ;
A79: G . o2 = x2 by A10, A76;
A80: G . o1 = x1 by A10, A74, A73;
then A81: (G . o1) + (G . o2) = addemb (g,x1,x2) by Def2, A79
.= g . (o1 + o2) by A78, A77, A12, Def1 ;
(G . o1) * (G . o2) = multemb (g,x1,x2) by Def4, A79, A80
.= g . (o1 * o2) by A78, A77, A12, Def3 ;
hence ( G . (o1 + o2) = (G . o1) + (G . o2) & G . (o1 * o2) = (G . o1) * (G . o2) ) by A81; :: thesis:

end;

suppose A82: ( 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
A83: 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, A82, XBOOLE_0:def 5;
then h . o2 in X by A4, FUNCT_1:def 3;
then consider x2 being Element of X such that
A84: 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;
A85: o1 = (g ") . (g . o1) by A11, A12, FUNCT_1:34
.= (g ") . x1 by A10, A83, A82 ;
A86: o2 = (g ") . (g . o2) by A11, A12, FUNCT_1:34
.= (g ") . x2 by A10, A84, A82 ;
A87: G . o1 = x1 by A10, A83, A82;
A88: G . o2 = x2 by A10, A84, A82;
then A89: (G . o1) + (G . o2) = addemb (g,x1,x2) by Def2, A87
.= g . (o1 + o2) by A86, A85, A12, Def1 ;
(G . o1) * (G . o2) = multemb (g,x1,x2) by Def4, A87, A88
.= g . (o1 * o2) by A86, A85, A12, Def3 ;
hence ( G . (o1 + o2) = (G . o1) + (G . o2) & G . (o1 * o2) = (G . o1) * (G . o2) ) by A89; :: thesis:

end;

then A90: ( G is additive & G is multiplicative ) ;
G is unity-preserving ;
hence G is linear by A90; :: thesis:

end;

A91: for o being object st o in [#] A holds
(G * f) . o = o

proof

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

end;

rng (id ([#] A)) c= ([#] A) \/ X by XBOOLE_1:7;
then reconsider i = id A as Function of (dom (id A)),C by FUNCT_2:2;
i is Function of A,C ;
then reconsider i = id A as Function of A,C ;
A96: G * f = i by A91;
G * f is RingHomomorphism by A1, A53, QUOFIELD:54;
then A is Subring of C by Th8, A96;
hence ex C being Ring 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 Subring of C & G is RingIsomorphism & id A = G * f ) by A4, A52, A96, A12, A53; :: thesis: