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:17;
f is RingMonomorphism by A1;
then consider h2 being Function of F9,F such that
A4: ( 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;
consider h3 being Function of F,F such that
h3 is RingHomomorphism and
h3 * f = f and
A5: for h9 being Function of F,F st h9 is RingHomomorphism & h9 * f = f holds
h9 = h3 by A1;
A6: (id F) * f = f by FUNCT_2:17;
f9 is RingMonomorphism by A2;
then consider h1 being Function of F,F9 such that
A7: h1 is RingHomomorphism and
A8: h1 * f = f9 and
for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h1 by A1;
( (h2 * h1) * f = f & h2 * h1 is RingHomomorphism ) by A7, A8, A4, Th54, RELAT_1:36;
then A9: h2 * h1 = h3 by A5
.= id the carrier of F by A6, A5 ;
consider h3 being Function of F9,F9 such that
h3 is RingHomomorphism and
h3 * f9 = f9 and
A10: for h9 being Function of F9,F9 st h9 is RingHomomorphism & h9 * f9 = f9 holds
h9 = h3 by A2;
( (h1 * h2) * f9 = f9 & h1 * h2 is RingHomomorphism ) by A7, A8, A4, Th54, RELAT_1:36;
then h1 * h2 = h3 by A10
.= id the carrier of F9 by A3, A10 ;
then rng h1 = the carrier of F9 by FUNCT_2:18;
then h1 is onto ;
then A11: h1 is RingEpimorphism by A7;
h1 is one-to-one by A9, FUNCT_2:31;
then h1 is RingMonomorphism by A7;
hence F is_ringisomorph_to F9 by A11; :: thesis: