let I be commutative domRing-like Ring; :: thesis:
let F, F9 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:
let f9 be Function of I,F9; :: thesis:
assume that
A1: I has_Field_of_Quotients_Pair F,f and
A2: I has_Field_of_Quotients_Pair F9,f9 ; :: thesis:
A3: (id F9) * f9 = f9 by FUNCT_2:23;
A4: f is RingMonomorphism by A1, Def29;
then consider h2 being Function of F9,F such that
A5: ( h2 is RingHomomorphism & h2 * f9 = f ) and
for h9 being Function of F9,F st h9 is RingHomomorphism & h9 * f9 = f holds
h9 = h2 by A2, Def29;
consider h3 being Function of F,F such that
h3 is RingHomomorphism and
h3 * f = f and
A6: for h9 being Function of F,F st h9 is RingHomomorphism & h9 * f = f holds
h9 = h3 by A1, A4, Def29;
A7: (id F) * f = f by FUNCT_2:23;
A8: f9 is RingMonomorphism by A2, Def29;
then consider h1 being Function of F,F9 such that
A9: h1 is RingHomomorphism and
A10: h1 * f = f9 and
for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h1 by A1, Def29;
( (h2 * h1) * f = f & h2 * h1 is RingHomomorphism ) by A9, A10, A5, Th57, RELAT_1:55;
then A11: h2 * h1 = h3 by A6
.= id the carrier of F by A7, A6 ;
consider h3 being Function of F9,F9 such that
h3 is RingHomomorphism and
h3 * f9 = f9 and
A12: for h9 being Function of F9,F9 st h9 is RingHomomorphism & h9 * f9 = f9 holds
h9 = h3 by A2, A8, Def29;
( (h1 * h2) * f9 = f9 & h1 * h2 is RingHomomorphism ) by A9, A10, A5, Th57, RELAT_1:55;
then h1 * h2 = h3 by A12
.= id the carrier of F9 by A3, A12 ;
then rng h1 = the carrier of F9 by FUNCT_2:24;
then A13: h1 is RingEpimorphism by A9, Def22;
h1 is one-to-one by A11, FUNCT_2:37;
then h1 is RingMonomorphism by A9, Def23;
hence F is_ringisomorph_to F9 by A13, Def26; :: thesis: