let I be commutative domRing-like Ring; :: thesis: for F, F' being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f being Function of I,F
for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
let F, F' be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for f being Function of I,F
for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
let f be Function of I,F; :: thesis: for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
let f' be Function of I,F'; :: thesis: ( I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' implies F is_ringisomorph_to F' )
assume A1: ( I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' ) ; :: thesis: F is_ringisomorph_to F'
then A2: f is RingMonomorphism by Def29;
A3: f' is RingMonomorphism by A1, Def29;
then consider h1 being Function of F,F' such that
A4: ( h1 is RingHomomorphism & h1 * f = f' & ( for h' being Function of F,F' st h' is RingHomomorphism & h' * f = f' holds
h' = h1 ) ) by A1, Def29;
consider h2 being Function of F',F such that
A5: ( h2 is RingHomomorphism & h2 * f' = f & ( for h' being Function of F',F st h' is RingHomomorphism & h' * f' = f holds
h' = h2 ) ) by A1, A2, Def29;
A6: (h2 * h1) * f = f by A4, A5, RELAT_1:55;
A7: h2 * h1 is RingHomomorphism by A4, A5, Th57;
A8: (id F) * f = f by FUNCT_2:23;
consider h3 being Function of F,F such that
A9: ( h3 is RingHomomorphism & h3 * f = f & ( for h' being Function of F,F st h' is RingHomomorphism & h' * f = f holds
h' = h3 ) ) by A1, A2, Def29;
h2 * h1 = h3 by A6, A7, A9
.= id the carrier of F by A8, A9 ;
then h1 is one-to-one by FUNCT_2:37;
then A10: h1 is RingMonomorphism by A4, Def23;
A11: (h1 * h2) * f' = f' by A4, A5, RELAT_1:55;
A12: h1 * h2 is RingHomomorphism by A4, A5, Th57;
A13: (id F') * f' = f' by FUNCT_2:23;
consider h3 being Function of F',F' such that
A14: ( h3 is RingHomomorphism & h3 * f' = f' & ( for h' being Function of F',F' st h' is RingHomomorphism & h' * f' = f' holds
h' = h3 ) ) by A1, A3, Def29;
h1 * h2 = h3 by A11, A12, A14
.= id the carrier of F' by A13, A14 ;
then rng h1 = the carrier of F' by FUNCT_2:24;
then h1 is RingEpimorphism by A4, Def22;
then h1 is RingIsomorphism by A10;
hence F is_ringisomorph_to F' by Def26; :: thesis: verum