let I be non degenerated commutative domRing-like Ring; :: thesis:
A1: canHom I is RingMonomorphism by Th60;

now

let F' be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis:
let f' be Function of I,F'; :: thesis:
assume A2: f' is RingMonomorphism ; :: thesis:
then f' is RingHomomorphism by Def23;
then A3: ( f' is additive & f' is multiplicative & f' is unity-preserving ) ;
set hh = { [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } ;
A4: { [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } is Relation-like

proof

for u being set st u in { [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } holds
ex a, b being set st u = [a,b]

proof

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

end;

hence { [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } is Relation-like by RELAT_1:def 1; :: thesis:

end;

{ [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } is Function-like

proof

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

proof

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

end;

hence { [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } is Function-like by FUNCT_1:def 1; :: thesis:

end;

then reconsider hh = { [[a,b],((f' . a) * ((f' . b) " ))] where a, b is Element of I : b <> 0. I } as Function by A4;
A11: dom hh = Q. I

proof

A12: 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
A13: [x,y] in hh by RELAT_1:def 4;
consider a, b being Element of I such that
A14: ( [x,y] = [[a,b],((f' . a) * ((f' . b) " ))] & b <> 0. I ) by A13;
x = [[a,b],((f' . a) * ((f' . b) " ))] `1 by A14, MCART_1:def 1
.= [a,b] by MCART_1:def 1 ;
hence x in Q. I by A14, 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
A15: ( x = [a,b] & b <> 0. I ) by Def1;
[[a,b],((f' . a) * ((f' . b) " ))] in hh by A15;
hence x in dom hh by A15, RELAT_1:def 4; :: thesis:

end;

hence dom hh = Q. I by A12, TARSKI:2; :: thesis:

end;

rng hh c= the carrier of F'

proof

for y being set st y in rng hh holds
y in the carrier of F'

proof

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

end;

hence rng hh c= the carrier of F' by TARSKI:def 3; :: thesis:

end;

then reconsider hh = hh as Function of Q. I,the carrier of F' by A11, FUNCT_2:def 1, RELSET_1:11;
A18: for x being Element of Q. I holds hh . x = (f' . (x `1 )) * ((f' . (x `2 )) " )

proof

let x be Element of Q. I; :: thesis:
consider a, b being Element of I such that
A19: ( x = [a,b] & b <> 0. I ) by Def1;
A20: ( x `1 = a & x `2 = b ) by A19, MCART_1:def 1, MCART_1:def 2;
[[a,b],((f' . a) * ((f' . b) " ))] in hh by A19;
hence hh . x = (f' . (x `1 )) * ((f' . (x `2 )) " ) by A11, A19, A20, FUNCT_1:def 4; :: thesis:

end;

set h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ;
A21: { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } is Relation-like

proof

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;

hence { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } is Relation-like by RELAT_1:def 1; :: thesis:

end;

{ [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } is Function-like

proof

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 A22: ( [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 } ) ; :: thesis:
then consider u1 being Element of Q. I such that
A23: ( [a,b1] = [(QClass. u1),(hh . u1)] & 1. I = 1. I ) ;
consider u2 being Element of Q. I such that
A24: ( [a,b2] = [(QClass. u2),(hh . u2)] & 1. I = 1. I ) by A22;
A25: a = [(QClass. u1),(hh . u1)] `1 by A23, MCART_1:def 1
.= QClass. u1 by MCART_1:def 1 ;
a = [(QClass. u2),(hh . u2)] `1 by A24, MCART_1:def 1
.= QClass. u2 by MCART_1:def 1 ;
then u1 in QClass. u2 by A25, Th6;
then A26: (u1 `1 ) * (u2 `2 ) = (u1 `2 ) * (u2 `1 ) by Def4;
f' is RingHomomorphism by A2, Def23;
then A27: ( f' is additive & f' is multiplicative & f' is unity-preserving ) ;
( u1 `2 <> 0. I & u2 `2 <> 0. I ) by Th2;
then A28: ( f' . (u1 `2 ) <> 0. F' & f' . (u2 `2 ) <> 0. F' ) by A2, Th54;
A29: hh . u1 = (f' . (u1 `1 )) / (f' . (u1 `2 )) by A18
.= ((f' . (u1 `1 )) / (f' . (u1 `2 ))) * (1. F') by VECTSP_1:def 16
.= ((f' . (u1 `1 )) / (f' . (u1 `2 ))) * ((f' . (u2 `2 )) / (f' . (u2 `2 ))) by A28, VECTSP_1:def 22
.= ((f' . (u1 `1 )) * (f' . (u2 `2 ))) / ((f' . (u1 `2 )) * (f' . (u2 `2 ))) by A28, Th51
.= (f' . ((u1 `2 ) * (u2 `1 ))) / ((f' . (u1 `2 )) * (f' . (u2 `2 ))) by A26, A27, GROUP_6:def 7
.= ((f' . (u1 `2 )) * (f' . (u2 `1 ))) / ((f' . (u1 `2 )) * (f' . (u2 `2 ))) by A27, GROUP_6:def 7
.= ((f' . (u1 `2 )) / (f' . (u1 `2 ))) * ((f' . (u2 `1 )) / (f' . (u2 `2 ))) by A28, Th51
.= (1. F') * ((f' . (u2 `1 )) * ((f' . (u2 `2 )) " )) by A28, VECTSP_1:def 22
.= (f' . (u2 `1 )) * ((f' . (u2 `2 )) " ) by VECTSP_1:def 16
.= hh . u2 by A18 ;
b1 = [(QClass. u1),(hh . u1)] `2 by A23, MCART_1:def 2
.= hh . u2 by A29, MCART_1:def 2
.= [a,b2] `2 by A24, MCART_1:def 2
.= b2 by MCART_1:def 2 ;
hence b1 = b2 ; :: thesis:

end;

hence { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } is Function-like by FUNCT_1:def 1; :: thesis:

end;

then reconsider h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } as Function by A21;
A30: dom h = Quot. I

proof

A31: 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
A32: [x,y] in h by RELAT_1:def 4;
consider u being Element of Q. I such that
A33: ( [x,y] = [(QClass. u),(hh . u)] & 1. I = 1. I ) by A32;
x = [(QClass. u),(hh . u)] `1 by A33, 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
A34: x = QClass. u by Def5;
[(QClass. u),(hh . u)] in h ;
hence x in dom h by A34, RELAT_1:def 4; :: thesis:

end;

hence dom h = Quot. I by A31, TARSKI:2; :: thesis:

end;

rng h c= the carrier of F'

proof

for y being set st y in rng h holds
y in the carrier of F'

proof

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

end;

hence rng h c= the carrier of F' by TARSKI:def 3; :: thesis:

end;

then reconsider h = h as Function of Quot. I,the carrier of F' by A30, FUNCT_2:def 1, RELSET_1:11;
reconsider h = h as Function of (the_Field_of_Quotients I),F' ;
A37: 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:
assume A38: x = QClass. u ; :: thesis:
[(QClass. u),(hh . u)] in h ;
hence h . x = hh . u by A30, A38, FUNCT_1:def 4; :: thesis:

end;

A39: ( 1_ I = 1. I & 1_ F' = 1. F' ) ;
A40: h is RingHomomorphism

proof

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_ F' )

proof

let x, y be Element of (the_Field_of_Quotients I); :: thesis:
reconsider x = x, y = y as Element of Quot. I ;
consider u being Element of Q. I such that
A41: x = QClass. u by Def5;
consider v being Element of Q. I such that
A42: y = QClass. v by Def5;
reconsider x = x, y = y as Element of (the_Field_of_Quotients I) ;
A43: ( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then A44: ( f' . (u `2 ) <> 0. F' & f' . (v `2 ) <> 0. F' ) by A2, Th54;
A45: (u `2 ) * (v `2 ) <> 0. I by A43, 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;
A46: (h . x) + (h . y) = (hh . u) + (h . y) by A37, A41
.= (hh . u) + (hh . v) by A37, A42
.= ((f' . (u `1 )) * ((f' . (u `2 )) " )) + (hh . v) by A18
.= ((f' . (u `1 )) / (f' . (u `2 ))) + ((f' . (v `1 )) / (f' . (v `2 ))) by A18
.= (((f' . (u `1 )) * (f' . (v `2 ))) + ((f' . (v `1 )) * (f' . (u `2 )))) / ((f' . (u `2 )) * (f' . (v `2 ))) by A44, Th52
.= ((f' . ((u `1 ) * (v `2 ))) + ((f' . (v `1 )) * (f' . (u `2 )))) / ((f' . (u `2 )) * (f' . (v `2 ))) by A3, GROUP_6:def 7
.= ((f' . ((u `1 ) * (v `2 ))) + (f' . ((v `1 ) * (u `2 )))) / ((f' . (u `2 )) * (f' . (v `2 ))) by A3, GROUP_6:def 7
.= ((f' . ((u `1 ) * (v `2 ))) + (f' . ((v `1 ) * (u `2 )))) * ((f' . ((u `2 ) * (v `2 ))) " ) by A3, GROUP_6:def 7
.= (f' . (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )))) * ((f' . ((u `2 ) * (v `2 ))) " ) by A3, GRCAT_1:def 13
.= (f' . (t `1 )) * ((f' . ((u `2 ) * (v `2 ))) " ) by MCART_1:def 1
.= (f' . (t `1 )) * ((f' . (t `2 )) " ) by MCART_1:def 2
.= hh . t by A18 ;
reconsider x' = x, y' = y as Element of Quot. I ;
A47: h . (qadd x',y') = h . (QClass. (padd u,v)) by A41, A42, Th11
.= h . (QClass. t) ;
A48: h . (QClass. t) = hh . t by A37;
reconsider t = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))] as Element of Q. I by A45, Def1;
A49: (h . x) * (h . y) = (hh . u) * (h . y) by A37, A41
.= (hh . u) * (hh . v) by A37, A42
.= ((f' . (u `1 )) * ((f' . (u `2 )) " )) * (hh . v) by A18
.= ((f' . (u `1 )) / (f' . (u `2 ))) * ((f' . (v `1 )) / (f' . (v `2 ))) by A18
.= ((f' . (u `1 )) * (f' . (v `1 ))) / ((f' . (u `2 )) * (f' . (v `2 ))) by A44, Th51
.= (f' . ((u `1 ) * (v `1 ))) / ((f' . (u `2 )) * (f' . (v `2 ))) by A3, GROUP_6:def 7
.= (f' . ((u `1 ) * (v `1 ))) * ((f' . ((u `2 ) * (v `2 ))) " ) by A3, GROUP_6:def 7
.= (f' . (t `1 )) * ((f' . ((u `2 ) * (v `2 ))) " ) by MCART_1:def 1
.= (f' . (t `1 )) * ((f' . (t `2 )) " ) by MCART_1:def 2
.= hh . t by A18 ;
reconsider x' = x, y' = y as Element of Quot. I ;
A50: h . (qmult x',y') = h . (QClass. (pmult u,v)) by A41, A42, Th12
.= h . (QClass. t) ;
A51: h . (QClass. t) = hh . t by A37;
A52: 0. F' <> 1. F' ;
0. I <> 1. I ;
then reconsider t = [(1. I),(1. I)] as Element of Q. I by Def1;
A53: q1. I = QClass. t

proof

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

proof

let u be set ; :: thesis:
assume A55: 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 A55, 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;

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

proof

let u be set ; :: thesis:
assume A56: 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 A56, 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;

hence q1. I = QClass. t by A54, TARSKI:2; :: thesis:

end;

h . (1_ (the_Field_of_Quotients I)) = hh . t by A37, A53
.= (f' . (t `1 )) * ((f' . (t `2 )) " ) by A18
.= (f' . (1. I)) * ((f' . (t `2 )) " ) by MCART_1:def 1
.= (f' . (1. I)) * ((f' . (1. I)) " ) by MCART_1:def 2
.= (1. F') * ((f' . (1_ I)) " ) by A3, A39, GROUP_1:def 17
.= (1. F') * ((1_ F') " ) by A3, GROUP_1:def 17
.= 1_ F' by A52, 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_ F' ) by A46, A47, A48, A49, A50, A51, Def12, Def13; :: thesis:

end;

then ( h is additive & h is multiplicative & h is unity-preserving ) by GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
hence h is RingHomomorphism ; :: thesis:

end;

A57: (1. F') " = 1. F'

proof

A58: 0. F' <> 1. F' ;
(1. F') * (1. F') = 1. F' by VECTSP_1:def 16;
hence (1. F') " = 1. F' by A58, VECTSP_1:def 22; :: thesis:

end;

A59: h * (canHom I) = f'

proof

A60: 0. I <> 1. I ;
A61: for x being set st x in dom f' holds
( x in dom (canHom I) & (canHom I) . x in dom h )

proof

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

end;

A63: for x being set st x in dom (canHom I) & (canHom I) . x in dom h holds
x in dom f'

proof

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

end;

for x being set st x in dom f' holds
f' . x = h . ((canHom I) . x)

proof

let x be set ; :: thesis:
assume x in dom f' ; :: thesis:
then reconsider x = x as Element of I ;
reconsider u = [x,(1. I)] as Element of Q. I by A60, Def1;
reconsider u' = QClass. u as Element of (the_Field_of_Quotients I) ;
h . ((canHom I) . x) = h . (QClass. (quotient x,(1. I))) by Def28
.= h . u' by Def27
.= hh . u by A37
.= (f' . (u `1 )) * ((f' . (u `2 )) " ) by A18
.= (f' . (u `1 )) * ((f' . (1_ I)) " ) by MCART_1:def 2
.= (f' . (u `1 )) * (1_ F') by A3, A57, GROUP_1:def 17
.= f' . (u `1 ) by VECTSP_1:def 16
.= f' . x by MCART_1:def 1 ;
hence f' . x = h . ((canHom I) . x) ; :: thesis:

end;

hence h * (canHom I) = f' by A61, A63, FUNCT_1:20; :: thesis:

end;

now

let h' be Function of (the_Field_of_Quotients I),F'; :: thesis:
assume A64: ( h' is RingHomomorphism & h' * (canHom I) = f' ) ; :: thesis:
A65: 0. I <> 1. I ;
for x being set st x in the carrier of (the_Field_of_Quotients I) holds
h' . 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 x' = x as Element of Quot. I ;
consider u being Element of Q. I such that
A66: x' = QClass. u by Def5;
consider a, b being Element of I such that
A67: ( u = [a,b] & b <> 0. I ) by Def1;
A68: h . x = hh . u by A37, A66
.= ((h' * (canHom I)) . (u `1 )) * ((f' . (u `2 )) " ) by A18, A64
.= (h' . ((canHom I) . (u `1 ))) * (((h' * (canHom I)) . (u `2 )) " ) by A64, FUNCT_2:21
.= (h' . ((canHom I) . (u `1 ))) * ((h' . ((canHom I) . (u `2 ))) " ) by FUNCT_2:21 ;
reconsider a' = [a,(1. I)], b' = [b,(1. I)] as Element of Q. I by A65, Def1;
reconsider a'' = QClass. a', b'' = QClass. b' as Element of (the_Field_of_Quotients I) ;
A69: b'' <> 0. (the_Field_of_Quotients I)

proof

assume A70: b'' = 0. (the_Field_of_Quotients I) ; :: thesis:
A71: b' in b'' by Th6;
b = b' `1 by MCART_1:def 1
.= 0. I by A70, A71, Def8 ;
hence contradiction by A67; :: thesis:

end;

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) ;
A72: (h' . ((canHom I) . (u `1 ))) * ((h' . ((canHom I) . (u `2 ))) " ) = (h' . ((canHom I) . a)) * ((h' . ((canHom I) . (u `2 ))) " ) by A67, MCART_1:def 1
.= (h' . aa) * ((h' . ((canHom I) . (u `2 ))) " ) by Def28
.= (h' . a'') * ((h' . ((canHom I) . (u `2 ))) " ) by A65, Def27
.= (h' . a'') * ((h' . ((canHom I) . b)) " ) by A67, MCART_1:def 2
.= (h' . a'') * ((h' . bb) " ) by Def28
.= (h' . a'') * ((h' . b'') " ) by A65, Def27
.= h' . (a'' * (b'' " )) by A64, A69, Th56 ;
reconsider bi = [(1. I),b] as Element of Q. I by A67, Def1;
reconsider bi' = QClass. bi as Element of (the_Field_of_Quotients I) ;
A73: h' . ((quotmult I) . a'',bi') = h' . (qmult (QClass. a'),(QClass. bi)) by Def13
.= h' . (QClass. (pmult a',bi)) by Th12 ;
pmult a',bi = u

proof

pmult a',bi = [(a * (bi `1 )),((a' `2 ) * (bi `2 ))] by MCART_1:def 1
.= [(a * (1. I)),((a' `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 ;
hence pmult a',bi = u by A67; :: thesis:

end;

hence h' . x = h . x by A66, A67, A68, A69, A72, A73, Th50; :: thesis:

end;

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

end;

hence ex h being Function of (the_Field_of_Quotients I),F' st
( h is RingHomomorphism & h * (canHom I) = f' & ( for h' being Function of (the_Field_of_Quotients I),F' st h' is RingHomomorphism & h' * (canHom I) = f' holds
h' = h ) ) by A40, A59; :: thesis:

end;

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: