let I be non degenerated commutative domRing-like Ring; :: thesis:

A1: now

let F9 be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis:
let f9 be Function of I,F9; :: thesis:
set hh = { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } ;
A2: for u being set st u in { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } holds
ex a, b being set st u = [a,b]

let u be set ; :: thesis:
assume u in { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } ; :: thesis:
then ex a, b being Element of I st
( u = [[a,b],((f9 . a) * ((f9 . b) " ))] & b <> 0. I ) ;
hence ex a, b being set st u = [a,b] ; :: thesis:

end;

for a, b1, b2 being set st [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } & [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } holds
b1 = b2

proof

let a, b1, b2 be set ; :: thesis:
assume that
A3: [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } and
A4: [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } ; :: thesis:
consider x1, x2 being Element of I such that
A5: [a,b1] = [[x1,x2],((f9 . x1) * ((f9 . x2) " ))] and
x2 <> 0. I by A3;
consider y1, y2 being Element of I such that
A6: [a,b2] = [[y1,y2],((f9 . y1) * ((f9 . y2) " ))] and
y2 <> 0. I by A4;
A7: a = [[y1,y2],((f9 . y1) * ((f9 . y2) " ))] `1 by A6, MCART_1:def 1
.= [y1,y2] by MCART_1:def 1 ;
A8: a = [[x1,x2],((f9 . x1) * ((f9 . x2) " ))] `1 by A5, MCART_1:def 1
.= [x1,x2] by MCART_1:def 1 ;
then A9: x2 = a `2 by MCART_1:def 2
.= y2 by A7, MCART_1:def 2 ;
x1 = a `1 by A8, MCART_1:def 1
.= y1 by A7, MCART_1:def 1 ;
then b1 = [a,b2] `2 by A5, A6, A9, MCART_1:def 2
.= b2 by MCART_1:def 2 ;
hence b1 = b2 ; :: thesis:

end;

then reconsider hh = { [[a,b],((f9 . a) * ((f9 . b) " ))] where a, b is Element of I : b <> 0. I } as Function by A2, FUNCT_1:def 1, RELAT_1:def 1;
A10: for x being set st x in dom hh holds
x in Q. I

proof

let x be set ; :: thesis:
assume x in dom hh ; :: thesis:
then consider y being set such that
A11: [x,y] in hh by RELAT_1:def 4;
consider a, b being Element of I such that
A12: [x,y] = [[a,b],((f9 . a) * ((f9 . b) " ))] and
A13: b <> 0. I by A11;
x = [[a,b],((f9 . a) * ((f9 . b) " ))] `1 by A12, MCART_1:def 1
.= [a,b] by MCART_1:def 1 ;
hence x in Q. I by A13, Def1; :: thesis:

end;

for x being set st x in Q. I holds
x in dom hh

proof

let x be set ; :: thesis:
assume x in Q. I ; :: thesis:
then consider a, b being Element of I such that
A14: x = [a,b] and
A15: b <> 0. I by Def1;
[[a,b],((f9 . a) * ((f9 . b) " ))] in hh by A15;
hence x in dom hh by A14, RELAT_1:def 4; :: thesis:

end;

then A16: dom hh = Q. I by A10, TARSKI:2;
for y being set st y in rng hh holds
y in the carrier of F9

proof

let y be set ; :: thesis:
assume y in rng hh ; :: thesis:
then consider x being set such that
A17: [x,y] in hh by RELAT_1:def 5;
consider a, b being Element of I such that
A18: [x,y] = [[a,b],((f9 . a) * ((f9 . b) " ))] and
b <> 0. I by A17;
y = [[a,b],((f9 . a) * ((f9 . b) " ))] `2 by A18, MCART_1:def 2
.= (f9 . a) * ((f9 . b) " ) by MCART_1:def 2 ;
hence y in the carrier of F9 ; :: thesis:

end;

then rng hh c= the carrier of F9 by TARSKI:def 3;
then reconsider hh = hh as Function of (Q. I),the carrier of F9 by A16, FUNCT_2:def 1, RELSET_1:11;
set h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ;
( 0. F9 <> 1. F9 & (1. F9) * (1. F9) = 1. F9 ) by VECTSP_1:def 16;
then A19: (1. F9) " = 1. F9 by VECTSP_1:def 22;
assume A20: f9 is RingMonomorphism ; :: thesis:
then A21: f9 is RingHomomorphism by Def23;
A22: for v being set st v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } holds
ex a, b being set st v = [a,b]

proof

let v be set ; :: thesis:
assume v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ; :: thesis:
then ex u being Element of Q. I st
( v = [(QClass. u),(hh . u)] & 1. I = 1. I ) ;
hence ex a, b being set st v = [a,b] ; :: thesis:

end;

A23: for x being Element of Q. I holds hh . x = (f9 . (x `1 )) * ((f9 . (x `2 )) " )

proof

let x be Element of Q. I; :: thesis:
consider a, b being Element of I such that
A24: x = [a,b] and
A25: b <> 0. I by Def1;
A26: [[a,b],((f9 . a) * ((f9 . b) " ))] in hh by A25;
( x `1 = a & x `2 = b ) by A24, MCART_1:def 1, MCART_1:def 2;
hence hh . x = (f9 . (x `1 )) * ((f9 . (x `2 )) " ) by A16, A24, A26, FUNCT_1:def 4; :: thesis:

end;

for a, b1, b2 being set st [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } & [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } holds
b1 = b2

proof

let a, b1, b2 be set ; :: thesis:
assume that
A27: [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } and
A28: [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ; :: thesis:
consider u1 being Element of Q. I such that
A29: [a,b1] = [(QClass. u1),(hh . u1)] and
1. I = 1. I by A27;
consider u2 being Element of Q. I such that
A30: [a,b2] = [(QClass. u2),(hh . u2)] and
1. I = 1. I by A28;
A31: a = [(QClass. u2),(hh . u2)] `1 by A30, MCART_1:def 1
.= QClass. u2 by MCART_1:def 1 ;
a = [(QClass. u1),(hh . u1)] `1 by A29, MCART_1:def 1
.= QClass. u1 by MCART_1:def 1 ;
then u1 in QClass. u2 by A31, Th6;
then A32: (u1 `1 ) * (u2 `2 ) = (u1 `2 ) * (u2 `1 ) by Def4;
u1 `2 <> 0. I by Th2;
then A33: f9 . (u1 `2 ) <> 0. F9 by A20, Th54;
u2 `2 <> 0. I by Th2;
then A34: f9 . (u2 `2 ) <> 0. F9 by A20, Th54;
A35: f9 is RingHomomorphism by A20, Def23;
A36: hh . u1 = (f9 . (u1 `1 )) / (f9 . (u1 `2 )) by A23
.= ((f9 . (u1 `1 )) / (f9 . (u1 `2 ))) * (1. F9) by VECTSP_1:def 16
.= ((f9 . (u1 `1 )) / (f9 . (u1 `2 ))) * ((f9 . (u2 `2 )) / (f9 . (u2 `2 ))) by A34, VECTSP_1:def 22
.= ((f9 . (u1 `1 )) * (f9 . (u2 `2 ))) / ((f9 . (u1 `2 )) * (f9 . (u2 `2 ))) by A33, A34, Th51
.= (f9 . ((u1 `2 ) * (u2 `1 ))) / ((f9 . (u1 `2 )) * (f9 . (u2 `2 ))) by A32, A35, GROUP_6:def 7
.= ((f9 . (u1 `2 )) * (f9 . (u2 `1 ))) / ((f9 . (u1 `2 )) * (f9 . (u2 `2 ))) by A35, GROUP_6:def 7
.= ((f9 . (u1 `2 )) / (f9 . (u1 `2 ))) * ((f9 . (u2 `1 )) / (f9 . (u2 `2 ))) by A33, A34, Th51
.= (1. F9) * ((f9 . (u2 `1 )) * ((f9 . (u2 `2 )) " )) by A33, VECTSP_1:def 22
.= (f9 . (u2 `1 )) * ((f9 . (u2 `2 )) " ) by VECTSP_1:def 16
.= hh . u2 by A23 ;
b1 = [(QClass. u1),(hh . u1)] `2 by A29, MCART_1:def 2
.= hh . u2 by A36, MCART_1:def 2
.= [a,b2] `2 by A30, MCART_1:def 2
.= b2 by MCART_1:def 2 ;
hence b1 = b2 ; :: thesis:

end;

then reconsider h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } as Function by A22, FUNCT_1:def 1, RELAT_1:def 1;
A37: for x being set st x in dom h holds
x in Quot. I

proof

let x be set ; :: thesis:
assume x in dom h ; :: thesis:
then consider y being set such that
A38: [x,y] in h by RELAT_1:def 4;
consider u being Element of Q. I such that
A39: [x,y] = [(QClass. u),(hh . u)] and
1. I = 1. I by A38;
x = [(QClass. u),(hh . u)] `1 by A39, MCART_1:def 1
.= QClass. u by MCART_1:def 1 ;
hence x in Quot. I ; :: thesis:

end;

for x being set st x in Quot. I holds
x in dom h

proof

let x be set ; :: thesis:
assume x in Quot. I ; :: thesis:
then consider u being Element of Q. I such that
A40: x = QClass. u by Def5;
[(QClass. u),(hh . u)] in h ;
hence x in dom h by A40, RELAT_1:def 4; :: thesis:

end;

then A41: dom h = Quot. I by A37, TARSKI:2;
for y being set st y in rng h holds
y in the carrier of F9

proof

let y be set ; :: thesis:
assume y in rng h ; :: thesis:
then consider x being set such that
A42: [x,y] in h by RELAT_1:def 5;
consider u being Element of Q. I such that
A43: [x,y] = [(QClass. u),(hh . u)] and
1. I = 1. I by A42;
y = [(QClass. u),(hh . u)] `2 by A43, MCART_1:def 2
.= hh . u by MCART_1:def 2 ;
hence y in the carrier of F9 ; :: thesis:

end;

then rng h c= the carrier of F9 by TARSKI:def 3;
then reconsider h = h as Function of (Quot. I),the carrier of F9 by A41, FUNCT_2:def 1, RELSET_1:11;
reconsider h = h as Function of (the_Field_of_Quotients I),F9 ;
A44: for x being Element of (the_Field_of_Quotients I)
for u being Element of Q. I st x = QClass. u holds
h . x = hh . u

proof

let x be Element of (the_Field_of_Quotients I); :: thesis:
let u be Element of Q. I; :: thesis:
A45: [(QClass. u),(hh . u)] in h ;
assume x = QClass. u ; :: thesis:
hence h . x = hh . u by A41, A45, FUNCT_1:def 4; :: thesis:

end;

A46: now

let h9 be Function of (the_Field_of_Quotients I),F9; :: thesis:
assume that
A47: h9 is RingHomomorphism and
A48: h9 * (canHom I) = f9 ; :: thesis:
A49: 0. I <> 1. I ;
for x being set st x in the carrier of (the_Field_of_Quotients I) holds
h9 . x = h . x

proof

let x be set ; :: thesis:
assume x in the carrier of (the_Field_of_Quotients I) ; :: thesis:
then reconsider x = x as Element of (the_Field_of_Quotients I) ;
reconsider x9 = x as Element of Quot. I ;
consider u being Element of Q. I such that
A50: x9 = QClass. u by Def5;
consider a, b being Element of I such that
A51: u = [a,b] and
A52: b <> 0. I by Def1;
reconsider a9 = [a,(1. I)], b9 = [b,(1. I)] as Element of Q. I by A49, Def1;
reconsider a99 = QClass. a9, b99 = QClass. b9 as Element of (the_Field_of_Quotients I) ;
reconsider bi = [(1. I),b] as Element of Q. I by A52, Def1;
reconsider aa = QClass. (quotient a,(1. I)) as Element of (the_Field_of_Quotients I) ;
reconsider bb = QClass. (quotient b,(1. I)) as Element of (the_Field_of_Quotients I) ;
reconsider bi9 = QClass. bi as Element of (the_Field_of_Quotients I) ;
A53: pmult a9,bi = [(a * (bi `1 )),((a9 `2 ) * (bi `2 ))] by MCART_1:def 1
.= [(a * (1. I)),((a9 `2 ) * (bi `2 ))] by MCART_1:def 1
.= [(a * (1. I)),((1. I) * (bi `2 ))] by MCART_1:def 2
.= [(a * (1. I)),((1. I) * b)] by MCART_1:def 2
.= [a,((1. I) * b)] by VECTSP_1:def 16
.= [a,b] by VECTSP_1:def 16 ;
A54: b99 <> 0. (the_Field_of_Quotients I)

proof

A55: b9 in b99 by Th6;
assume A56: b99 = 0. (the_Field_of_Quotients I) ; :: thesis:
b = b9 `1 by MCART_1:def 1
.= 0. I by A56, A55, Def8 ;
hence contradiction by A52; :: thesis:

end;

A57: h . x = hh . u by A44, A50
.= ((h9 * (canHom I)) . (u `1 )) * ((f9 . (u `2 )) " ) by A23, A48
.= (h9 . ((canHom I) . (u `1 ))) * (((h9 * (canHom I)) . (u `2 )) " ) by A48, FUNCT_2:21
.= (h9 . ((canHom I) . (u `1 ))) * ((h9 . ((canHom I) . (u `2 ))) " ) by FUNCT_2:21 ;
A58: h9 . ((quotmult I) . a99,bi9) = h9 . (qmult (QClass. a9),(QClass. bi)) by Def13
.= h9 . (QClass. (pmult a9,bi)) by Th12 ;
(h9 . ((canHom I) . (u `1 ))) * ((h9 . ((canHom I) . (u `2 ))) " ) = (h9 . ((canHom I) . a)) * ((h9 . ((canHom I) . (u `2 ))) " ) by A51, MCART_1:def 1
.= (h9 . aa) * ((h9 . ((canHom I) . (u `2 ))) " ) by Def28
.= (h9 . a99) * ((h9 . ((canHom I) . (u `2 ))) " ) by A49, Def27
.= (h9 . a99) * ((h9 . ((canHom I) . b)) " ) by A51, MCART_1:def 2
.= (h9 . a99) * ((h9 . bb) " ) by Def28
.= (h9 . a99) * ((h9 . b99) " ) by A49, Def27
.= h9 . (a99 * (b99 " )) by A47, A54, Th56 ;
hence h9 . x = h . x by A50, A51, A52, A57, A54, A58, A53, Th50; :: thesis:

end;

hence h9 = h by FUNCT_2:18; :: thesis:

end;

A59: 1_ F9 = 1. F9 ;
for x, y being Element of (the_Field_of_Quotients I) holds
( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 )

proof

let x, y be Element of (the_Field_of_Quotients I); :: thesis:
reconsider x = x, y = y as Element of Quot. I ;
A60: 0. F9 <> 1. F9 ;
consider u being Element of Q. I such that
A61: x = QClass. u by Def5;
A62: u `2 <> 0. I by Th2;
then A63: f9 . (u `2 ) <> 0. F9 by A20, Th54;
consider v being Element of Q. I such that
A64: y = QClass. v by Def5;
A65: v `2 <> 0. I by Th2;
then A66: f9 . (v `2 ) <> 0. F9 by A20, Th54;
A67: (u `2 ) * (v `2 ) <> 0. I by A62, A65, VECTSP_2:def 5;
then reconsider t = [(((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))),((u `2 ) * (v `2 ))] as Element of Q. I by Def1;
reconsider x = x, y = y as Element of (the_Field_of_Quotients I) ;
reconsider x9 = x, y9 = y as Element of Quot. I ;
A68: h . (qadd x9,y9) = h . (QClass. (padd u,v)) by A61, A64, Th11
.= h . (QClass. t) ;
A69: (h . x) + (h . y) = (hh . u) + (h . y) by A44, A61
.= (hh . u) + (hh . v) by A44, A64
.= ((f9 . (u `1 )) * ((f9 . (u `2 )) " )) + (hh . v) by A23
.= ((f9 . (u `1 )) / (f9 . (u `2 ))) + ((f9 . (v `1 )) / (f9 . (v `2 ))) by A23
.= (((f9 . (u `1 )) * (f9 . (v `2 ))) + ((f9 . (v `1 )) * (f9 . (u `2 )))) / ((f9 . (u `2 )) * (f9 . (v `2 ))) by A63, A66, Th52
.= ((f9 . ((u `1 ) * (v `2 ))) + ((f9 . (v `1 )) * (f9 . (u `2 )))) / ((f9 . (u `2 )) * (f9 . (v `2 ))) by A21, GROUP_6:def 7
.= ((f9 . ((u `1 ) * (v `2 ))) + (f9 . ((v `1 ) * (u `2 )))) / ((f9 . (u `2 )) * (f9 . (v `2 ))) by A21, GROUP_6:def 7
.= ((f9 . ((u `1 ) * (v `2 ))) + (f9 . ((v `1 ) * (u `2 )))) * ((f9 . ((u `2 ) * (v `2 ))) " ) by A21, GROUP_6:def 7
.= (f9 . (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )))) * ((f9 . ((u `2 ) * (v `2 ))) " ) by A21, GRCAT_1:def 13
.= (f9 . (t `1 )) * ((f9 . ((u `2 ) * (v `2 ))) " ) by MCART_1:def 1
.= (f9 . (t `1 )) * ((f9 . (t `2 )) " ) by MCART_1:def 2
.= hh . t by A23 ;
A70: h . (QClass. t) = hh . t by A44;
reconsider t = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))] as Element of Q. I by A67, Def1;
A71: (h . x) * (h . y) = (hh . u) * (h . y) by A44, A61
.= (hh . u) * (hh . v) by A44, A64
.= ((f9 . (u `1 )) * ((f9 . (u `2 )) " )) * (hh . v) by A23
.= ((f9 . (u `1 )) / (f9 . (u `2 ))) * ((f9 . (v `1 )) / (f9 . (v `2 ))) by A23
.= ((f9 . (u `1 )) * (f9 . (v `1 ))) / ((f9 . (u `2 )) * (f9 . (v `2 ))) by A63, A66, Th51
.= (f9 . ((u `1 ) * (v `1 ))) / ((f9 . (u `2 )) * (f9 . (v `2 ))) by A21, GROUP_6:def 7
.= (f9 . ((u `1 ) * (v `1 ))) * ((f9 . ((u `2 ) * (v `2 ))) " ) by A21, GROUP_6:def 7
.= (f9 . (t `1 )) * ((f9 . ((u `2 ) * (v `2 ))) " ) by MCART_1:def 1
.= (f9 . (t `1 )) * ((f9 . (t `2 )) " ) by MCART_1:def 2
.= hh . t by A23 ;
reconsider x9 = x, y9 = y as Element of Quot. I ;
A72: h . (qmult x9,y9) = h . (QClass. (pmult u,v)) by A61, A64, Th12
.= h . (QClass. t) ;
A73: h . (QClass. t) = hh . t by A44;
0. I <> 1. I ;
then reconsider t = [(1. I),(1. I)] as Element of Q. I by Def1;
A74: for u being set st u in QClass. t holds
u in q1. I

proof

let u be set ; :: thesis:
assume A75: u in QClass. t ; :: thesis:
then reconsider u = u as Element of Q. I ;
u `1 = (u `1 ) * (1. I) by VECTSP_1:def 16
.= (u `1 ) * (t `2 ) by MCART_1:def 2
.= (u `2 ) * (t `1 ) by A75, Def4
.= (u `2 ) * (1. I) by MCART_1:def 1
.= u `2 by VECTSP_1:def 16 ;
hence u in q1. I by Def9; :: thesis:

end;

for u being set st u in q1. I holds
u in QClass. t

proof

let u be set ; :: thesis:
assume A76: u in q1. I ; :: thesis:
then reconsider u = u as Element of Q. I ;
(u `1 ) * (t `2 ) = (u `1 ) * (1. I) by MCART_1:def 2
.= u `1 by VECTSP_1:def 16
.= u `2 by A76, Def9
.= (u `2 ) * (1. I) by VECTSP_1:def 16
.= (u `2 ) * (t `1 ) by MCART_1:def 1 ;
hence u in QClass. t by Def4; :: thesis:

end;

then q1. I = QClass. t by A74, TARSKI:2;
then h . (1_ (the_Field_of_Quotients I)) = hh . t by A44
.= (f9 . (t `1 )) * ((f9 . (t `2 )) " ) by A23
.= (f9 . (1. I)) * ((f9 . (t `2 )) " ) by MCART_1:def 1
.= (f9 . (1. I)) * ((f9 . (1. I)) " ) by MCART_1:def 2
.= (1. F9) * ((f9 . (1_ I)) " ) by A21, A59, GROUP_1:def 17
.= (1. F9) * ((1_ F9) " ) by A21, GROUP_1:def 17
.= 1_ F9 by A60, VECTSP_1:def 22 ;
hence ( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 ) by A69, A68, A70, A71, A72, A73, Def12, Def13; :: thesis:

end;

then A77: ( h is additive & h is multiplicative & h is unity-preserving ) by GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
A78: for x being set st x in dom f9 holds
( x in dom (canHom I) & (canHom I) . x in dom h )

proof

let x be set ; :: thesis:
assume x in dom f9 ; :: thesis:
then reconsider x = x as Element of I ;
dom h = the carrier of (the_Field_of_Quotients I) by FUNCT_2:def 1;
then ( x in the carrier of I & (canHom I) . x in dom h ) ;
hence ( x in dom (canHom I) & (canHom I) . x in dom h ) by FUNCT_2:def 1; :: thesis:

end;

A79: 0. I <> 1. I ;
A80: for x being set st x in dom f9 holds
f9 . x = h . ((canHom I) . x)

proof

let x be set ; :: thesis:
assume x in dom f9 ; :: thesis:
then reconsider x = x as Element of I ;
reconsider u = [x,(1. I)] as Element of Q. I by A79, Def1;
reconsider u9 = QClass. u as Element of (the_Field_of_Quotients I) ;
h . ((canHom I) . x) = h . (QClass. (quotient x,(1. I))) by Def28
.= h . u9 by Def27
.= hh . u by A44
.= (f9 . (u `1 )) * ((f9 . (u `2 )) " ) by A23
.= (f9 . (u `1 )) * ((f9 . (1_ I)) " ) by MCART_1:def 2
.= (f9 . (u `1 )) * (1_ F9) by A21, A19, GROUP_1:def 17
.= f9 . (u `1 ) by VECTSP_1:def 16
.= f9 . x by MCART_1:def 1 ;
hence f9 . x = h . ((canHom I) . x) ; :: thesis:

end;

for x being set st x in dom (canHom I) & (canHom I) . x in dom h holds
x in dom f9

proof

let x be set ; :: thesis:
assume that
A81: x in dom (canHom I) and
(canHom I) . x in dom h ; :: thesis:
reconsider x = x as Element of I by A81;
x in the carrier of I ;
hence x in dom f9 by FUNCT_2:def 1; :: thesis:

end;

then h * (canHom I) = f9 by A78, A80, FUNCT_1:20;
hence ex h being Function of (the_Field_of_Quotients I),F9 st
( h is RingHomomorphism & h * (canHom I) = f9 & ( for h9 being Function of (the_Field_of_Quotients I),F9 st h9 is RingHomomorphism & h9 * (canHom I) = f9 holds
h9 = h ) ) by A77, A46; :: thesis:

end;

canHom I is RingMonomorphism by Th60;
then I has_Field_of_Quotients_Pair the_Field_of_Quotients I, canHom I by A1, Def29;
hence ex F being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ex f being Function of I,F st I has_Field_of_Quotients_Pair F,f ; :: thesis: