:: The Field of Quotients over an Integral Domain
::  by Christoph Schwarzweller
::
:: Received May 4, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, STRUCT_0, SUBSET_1, ZFMISC_1, SUPINF_2, ALGSTR_0,
      MESFUNC1, MCART_1, VECTSP_2, RELAT_1, ARYTM_3, BINOP_1, RLVECT_1,
      LATTICES, SETFAM_1, FUNCSDOM, GROUP_1, ARYTM_1, FUNCT_1, VECTSP_1,
      MSSUBFAM, TARSKI, QUOFIELD, FUNCT_2, FDIFF_1, MOD_4;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, BINOP_1, DOMAIN_1,
      STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_2, VECTSP_1, TOPS_2,
      GRCAT_1, GCD_1, GROUP_6, RINGCAT1, MOD_4;
 constructors DOMAIN_1, TOPS_2, GRCAT_1, GROUP_6, GCD_1, ALGSTR_1, RELSET_1,
      XTUPLE_0, RINGCAT1, MOD_4;
 registrations SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1, ALGSTR_1,
      GCD_1, XTUPLE_0, RINGCAT1, MOD_4;
 requirements SUBSET, BOOLE;


begin :: Definition of Pairs

definition
  let I be non empty ZeroStr;
  func Q.I -> Subset of [:the carrier of I,the carrier of I:] means
:: QUOFIELD:def 1

  for u being set holds
  u in it iff ex a,b being Element of I st u = [a,b] & b <> 0.I;
end;

theorem :: QUOFIELD:1
  for I being non degenerated non empty multLoopStr_0 holds Q.I is non empty;

registration
  let I be non degenerated non empty multLoopStr_0;
  cluster Q.I -> non empty;
end;

theorem :: QUOFIELD:2
  for I being non degenerated non empty multLoopStr_0 for u being
  Element of Q.I holds u`2 <> 0.I;

:: Definition and some Properties of Pair Addition and Multiplication

definition
  let I be non degenerated domRing-like non empty doubleLoopStr;
  let u,v be Element of Q.I;
  func padd(u,v) -> Element of Q.I equals
:: QUOFIELD:def 2
  [u`1 * v`2 + v`1 * u`2, u`2 * v`2];
end;

definition
  let I be non degenerated domRing-like non empty doubleLoopStr;
  let u,v be Element of Q.I;
  func pmult(u,v) -> Element of Q.I equals
:: QUOFIELD:def 3
  [u`1 * v`1, u`2 * v`2];
end;

theorem :: QUOFIELD:3
  for I being non degenerated domRing-like associative commutative
Abelian add-associative distributive non empty doubleLoopStr for u,v,w being
Element of Q.I holds padd(u,padd(v,w)) = padd(padd(u,v),w);

theorem :: QUOFIELD:4
  for I being non degenerated domRing-like associative commutative
Abelian non empty doubleLoopStr for u,v,w being Element of Q.I holds pmult(u,
  pmult(v,w)) = pmult(pmult(u,v),w);

definition
  let I be non degenerated domRing-like associative commutative Abelian
  add-associative distributive non empty doubleLoopStr;
  let u, v be Element of Q.I;
  redefine func padd(u,v);
  commutativity;
end;

definition
  let I be non degenerated domRing-like associative commutative Abelian non
  empty doubleLoopStr;
  let u, v be Element of Q.I;
  redefine func pmult(u,v);
  commutativity;
end;

:: Definition of Classes of Pairs

definition
  let I be non degenerated non empty multLoopStr_0;
  let u be Element of Q.I;
  func QClass.u -> Subset of Q.I means
:: QUOFIELD:def 4

  for z being Element of Q.I holds z in it iff z`1 * u`2 = z`2 * u`1;
end;

theorem :: QUOFIELD:5
  for I being non degenerated commutative non empty multLoopStr_0
  for u being Element of Q.I holds u in QClass.u;

registration
  let I be non degenerated commutative non empty multLoopStr_0;
  let u be Element of Q.I;
  cluster QClass.u -> non empty;
end;

definition
  let I be non degenerated non empty multLoopStr_0;
  func Quot.I -> Subset-Family of Q.I means
:: QUOFIELD:def 5

  for A being Subset of Q.I
  holds A in it iff ex u being Element of Q.I st A = QClass.u;
end;

theorem :: QUOFIELD:6
  for I being non degenerated non empty multLoopStr_0 holds Quot.
  I is non empty;

registration
  let I be non degenerated non empty multLoopStr_0;
  cluster Quot.I -> non empty;
end;

theorem :: QUOFIELD:7
  for I being non degenerated domRing-like commutative Ring for u,v
  being Element of Q.I holds (ex w being Element of Quot.I st u in w & v in w)
  implies u`1 * v`2 = v`1 * u`2;

theorem :: QUOFIELD:8
  for I being non degenerated domRing-like commutative Ring for u,v
  being Element of Quot.I holds u meets v implies u = v;

begin :: Definition of Quotient Field Addition and Multiplication

definition
  let I be non degenerated domRing-like commutative Ring;
  let u,v be Element of Quot.I;
  func qadd(u,v) -> Element of Quot.I means
:: QUOFIELD:def 6

  for z being Element of Q.I
holds z in it iff ex a,b being Element of Q.I st a in u & b in v & z`1 * (a`2 *
  b`2) = z`2 * (a`1 * b`2 + b`1 * a`2);
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  let u,v be Element of Quot.I;
  func qmult(u,v) -> Element of Quot.I means
:: QUOFIELD:def 7

  for z being Element of Q.I
holds z in it iff ex a,b being Element of Q.I st a in u & b in v & z`1 * (a`2 *
  b`2) = z`2 * (a`1 * b`1);
end;

definition
  let I be non degenerated non empty multLoopStr_0;
  let u be Element of Q.I;
  redefine func QClass.u -> Element of Quot.I;
end;

theorem :: QUOFIELD:9
  for I being non degenerated domRing-like commutative Ring for u,
  v being Element of Q.I holds qadd(QClass.u,QClass.v) = QClass.(padd(u,v));

theorem :: QUOFIELD:10
  for I being non degenerated domRing-like commutative Ring for u,
  v being Element of Q.I holds qmult(QClass.u,QClass.v) = QClass.(pmult(u,v));

:: Properties of Quotient Field Addition and Multiplication

definition
  let I be non degenerated domRing-like commutative Ring;
  func q0.I -> Element of Quot.I means
:: QUOFIELD:def 8

  for z being Element of Q.I holds z in it iff z`1 = 0.I;
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  func q1.I -> Element of Quot.I means
:: QUOFIELD:def 9

  for z being Element of Q.I holds z in it iff z`1 = z`2;
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  let u be Element of Quot.I;
  func qaddinv(u) -> Element of Quot.I means
:: QUOFIELD:def 10

  for z being Element of Q.
I holds z in it iff ex a being Element of Q.I st a in u & z`1 * a`2 = z`2 * (-(
  a`1));
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  let u be Element of Quot.I;
  assume
 u <> q0.I;
  func qmultinv(u) -> Element of Quot.I means
:: QUOFIELD:def 11

  for z being Element of
Q.I holds z in it iff ex a being Element of Q.I st a in u & z`1 * a`1 = z`2 * a
  `2;
end;

theorem :: QUOFIELD:11
  for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qadd(u,qadd(v,w)) = qadd(qadd(u,v),w) & qadd(
  u,v) = qadd(v,u);

theorem :: QUOFIELD:12
  for I being non degenerated domRing-like commutative Ring for u
  being Element of Quot.I holds qadd(u,q0.I) = u & qadd(q0.I,u) = u;

theorem :: QUOFIELD:13
  for I being non degenerated domRing-like commutative Ring for u,
  v,w being Element of Quot.I holds qmult(u,qmult(v,w)) = qmult(qmult(u,v),w) &
  qmult(u,v) = qmult(v,u);

theorem :: QUOFIELD:14
  for I being non degenerated domRing-like commutative Ring for u
  being Element of Quot.I holds qmult(u,q1.I) = u & qmult(q1.I,u) = u;

theorem :: QUOFIELD:15
  for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qmult(qadd(u,v),w) = qadd(qmult(u,w),qmult(v,
  w));

theorem :: QUOFIELD:16
  for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qmult(u,qadd(v,w)) = qadd(qmult(u,v),qmult(u,
  w));

theorem :: QUOFIELD:17
  for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds qadd(u,qaddinv(u)) = q0.I & qadd(qaddinv(u),u) =
  q0.I;

theorem :: QUOFIELD:18
  for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I st u <> q0.I holds qmult(u,qmultinv(u)) = q1.I & qmult(
  qmultinv(u),u) = q1.I;

theorem :: QUOFIELD:19
  for I being non degenerated domRing-like commutative Ring holds q1.I <> q0.I;

:: Redefinition of the Operations' Types

definition
  let I be non degenerated domRing-like commutative Ring;
  func quotadd(I) -> BinOp of Quot.I means
:: QUOFIELD:def 12

  for u,v being Element of Quot.I holds it.(u,v) = qadd(u,v);
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  func quotmult(I) -> BinOp of Quot.I means
:: QUOFIELD:def 13

  for u,v being Element of Quot.I holds it.(u,v) = qmult(u,v);
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  func quotaddinv(I) -> UnOp of Quot.I means
:: QUOFIELD:def 14

  for u being Element of Quot.I holds it.(u) = qaddinv(u);
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  func quotmultinv(I) -> UnOp of Quot.I means
:: QUOFIELD:def 15

  for u being Element of Quot.I holds it.(u) = qmultinv(u);
end;

theorem :: QUOFIELD:20
  for I being non degenerated domRing-like commutative Ring for u,
  v,w being Element of Quot.I holds (quotadd(I)).((quotadd(I)).(u,v),w) = (
  quotadd(I)).(u,(quotadd(I)).(v,w));

theorem :: QUOFIELD:21
  for I being non degenerated domRing-like commutative Ring for u,
  v being Element of Quot.I holds (quotadd(I)).(u,v) = (quotadd(I)).(v,u);

theorem :: QUOFIELD:22
  for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds (quotadd(I)).(u,q0.I) = u & (quotadd(I)).(q0.I,u)
  = u;

theorem :: QUOFIELD:23
  for I being non degenerated domRing-like commutative Ring for u,
  v,w being Element of Quot.I holds (quotmult(I)).((quotmult(I)).(u,v),w) = (
  quotmult(I)).(u,(quotmult(I)).(v,w));

theorem :: QUOFIELD:24
  for I being non degenerated domRing-like commutative Ring for u,
  v being Element of Quot.I holds (quotmult(I)).(u,v)=(quotmult(I)).(v,u);

theorem :: QUOFIELD:25
  for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds (quotmult(I)).(u,q1.I) = u & (quotmult(I)).(q1.I,
  u) = u;

theorem :: QUOFIELD:26
  for I being non degenerated domRing-like commutative Ring for u,
  v,w being Element of Quot.I holds (quotmult(I)).((quotadd(I)).(u,v),w) = (
  quotadd(I)).((quotmult(I)).(u,w),(quotmult(I)).(v,w));

theorem :: QUOFIELD:27
  for I being non degenerated domRing-like commutative Ring for u,
  v,w being Element of Quot.I holds (quotmult(I)).(u,(quotadd(I)).(v,w)) = (
  quotadd(I)).((quotmult(I)).(u,v),(quotmult(I)).(u,w));

theorem :: QUOFIELD:28
  for I being non degenerated domRing-like commutative Ring for u
  being Element of Quot.I holds (quotadd(I)).(u,(quotaddinv(I)).(u)) = q0.I & (
  quotadd(I)).((quotaddinv(I)).(u),u) = q0.I;

theorem :: QUOFIELD:29
  for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I st u <> q0.I holds (quotmult(I)).(u,(quotmultinv(I)).(u
  )) = q1.I & (quotmult(I)).((quotmultinv(I)).(u),u) = q1.I;

begin :: Definition of Quotient Field

definition
  let I be non degenerated domRing-like commutative Ring;
  func the_Field_of_Quotients(I) -> strict doubleLoopStr equals
:: QUOFIELD:def 16
  doubleLoopStr
  (# Quot.I,quotadd(I),quotmult(I),q1.I,q0.I #);
end;

registration
  let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) -> non empty;
end;

theorem :: QUOFIELD:30
  for I being non degenerated domRing-like commutative Ring holds the
  carrier of the_Field_of_Quotients(I) = Quot.I & the addF of
the_Field_of_Quotients(I) = quotadd(I) & the multF of the_Field_of_Quotients(I)
= quotmult(I) & 0.the_Field_of_Quotients(I) = q0.I & 1.the_Field_of_Quotients(I
  ) = q1.I;

theorem :: QUOFIELD:31
  for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds (quotadd(I)).(u,v) is Element
  of the_Field_of_Quotients(I);

theorem :: QUOFIELD:32
  for I being non degenerated domRing-like commutative Ring for u
being Element of the_Field_of_Quotients(I) holds (quotaddinv(I)).(u) is Element
  of the_Field_of_Quotients(I);

theorem :: QUOFIELD:33
  for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds (quotmult(I)).(u,v) is Element
  of the_Field_of_Quotients(I);

theorem :: QUOFIELD:34
  for I being non degenerated domRing-like commutative Ring for u being
  Element of the_Field_of_Quotients(I) holds (quotmultinv(I)).(u) is Element of
  the_Field_of_Quotients(I);

theorem :: QUOFIELD:35
  for I being non degenerated domRing-like commutative Ring for u,v
  being Element of the_Field_of_Quotients(I) holds u + v = (quotadd(I)).(u,v);

registration
  let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) -> add-associative right_zeroed
    right_complementable;
end;

theorem :: QUOFIELD:36
  for I being non degenerated domRing-like commutative Ring for u being
  Element of the_Field_of_Quotients(I) holds -u = (quotaddinv(I)).(u);

theorem :: QUOFIELD:37
  for I being non degenerated domRing-like commutative Ring for u,v
  being Element of the_Field_of_Quotients(I) holds u * v = (quotmult(I)).(u,v);

registration
  let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) -> commutative;
end;

registration
  let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) -> well-unital;
end;

theorem :: QUOFIELD:38
  for I being non degenerated domRing-like commutative Ring holds 1.
  the_Field_of_Quotients(I) = q1.I & 0.the_Field_of_Quotients(I) = q0.I;

theorem :: QUOFIELD:39
  for I being non degenerated domRing-like commutative Ring for u,v,w
  being Element of the_Field_of_Quotients(I) holds (u + v) + w = u + (v + w);

theorem :: QUOFIELD:40
  for I being non degenerated domRing-like commutative Ring for u,v
  being Element of the_Field_of_Quotients(I) holds u + v = v + u;

theorem :: QUOFIELD:41
  for I being non degenerated domRing-like commutative Ring for u being
Element of the_Field_of_Quotients(I) holds u + 0.the_Field_of_Quotients(I) = u;

theorem :: QUOFIELD:42
  for I being non degenerated domRing-like commutative Ring for u being
Element of the_Field_of_Quotients(I) holds 1.the_Field_of_Quotients(I) * u = u;

theorem :: QUOFIELD:43
  for I being non degenerated domRing-like commutative Ring for u,v
  being Element of the_Field_of_Quotients(I) holds u * v = v * u;

theorem :: QUOFIELD:44
  for I being non degenerated domRing-like commutative Ring for u,v,w
  being Element of the_Field_of_Quotients(I) holds (u * v) * w = u * (v * w);

theorem :: QUOFIELD:45
  for I being non degenerated domRing-like commutative Ring for u
being Element of the_Field_of_Quotients(I) st u <> 0.the_Field_of_Quotients(I)
  ex v being Element of the_Field_of_Quotients(I) st u * v = 1.
  the_Field_of_Quotients(I);

theorem :: QUOFIELD:46
  for I being non degenerated domRing-like commutative Ring holds
the_Field_of_Quotients(I) is add-associative right_zeroed right_complementable
Abelian associative unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr;

registration
  let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) -> Abelian associative distributive
    almost_left_invertible non degenerated;
end;

theorem :: QUOFIELD:47
  for I being non degenerated domRing-like commutative Ring for x
being Element of the_Field_of_Quotients(I) st x <> 0.the_Field_of_Quotients(I)
for a being Element of I st a <> 0.I for u being Element of Q.I st x = QClass.u
  & u = [a,1.I] for v being Element of Q.I st v = [1.I,a] holds x" = QClass.v;

:: Field is Integral Domain

registration
  cluster -> domRing-like right_unital for add-associative right_zeroed
    right_complementable commutative associative well-unital distributive
    almost_left_invertible non empty doubleLoopStr;
end;

registration
  cluster add-associative right_zeroed right_complementable Abelian
    commutative associative left_unital distributive almost_left_invertible non
    degenerated for non empty doubleLoopStr;
end;

definition
  let F be commutative associative well-unital distributive
  almost_left_invertible non empty doubleLoopStr;
  let x, y be Element of F;
  func x/y -> Element of F equals
:: QUOFIELD:def 17
  x * y";
end;

theorem :: QUOFIELD:48
  for F being non degenerated almost_left_invertible commutative
Ring for a,b,c,d being Element of F st b <> 0.F & d <> 0.F holds (a/b) * (c/d)
  = (a * c) / (b * d);

theorem :: QUOFIELD:49
  for F being non degenerated almost_left_invertible commutative
Ring for a,b,c,d being Element of F st b <> 0.F & d <> 0.F holds (a/b) + (c/d)
  = (a*d + c*b) / (b * d);

begin :: Definition of Ring Homomorphism

notation
  let R,S be non empty doubleLoopStr;
  let f be Function of R, S;
  synonym f is RingHomomorphism for f is linear;
  synonym f is RingEpimorphism for f is epimorphism;
  synonym f is RingMonomorphism for f is monomorphism;
end;

notation
  let R,S be non empty doubleLoopStr;
  let f be Function of R, S;
  synonym f is embedding for f is RingMonomorphism;
  synonym f is RingIsomorphism for f is isomorphism;
end;

theorem :: QUOFIELD:50
  for R,S being Ring for f being Function of R, S st
  f is RingHomomorphism holds f.(0.R) = 0.S;

theorem :: QUOFIELD:51
  for R,S being Ring for f being Function of R, S st f is
  RingMonomorphism for x being Element of R holds f.x = 0.S iff x = 0.R;

theorem :: QUOFIELD:52
  for R,S being non degenerated almost_left_invertible commutative
Ring for f being Function of R, S st f is RingHomomorphism for x being Element
  of R st x <> 0.R holds f.(x") = (f.x)";

theorem :: QUOFIELD:53
  for R,S being non degenerated almost_left_invertible commutative
  Ring for f being Function of R, S st f is RingHomomorphism for x,y being
  Element of R st y <> 0.R holds f.(x * y") = f.x * (f.y)";

theorem :: QUOFIELD:54
  for R,S,T being Ring for f being Function of R, S st f is
RingHomomorphism for g being Function of S, T st g is RingHomomorphism holds g*
  f is RingHomomorphism;

theorem :: QUOFIELD:55
  for R being non empty doubleLoopStr holds id R is RingHomomorphism;

registration
  let R be non empty doubleLoopStr;
  cluster id R -> RingHomomorphism;
end;

definition
::$CD 4
  let R,S be non empty doubleLoopStr;
  pred R is_embedded_in S means
:: QUOFIELD:def 22
  ex f being Function of R, S st f is RingMonomorphism;
end;

definition
  let R,S be non empty doubleLoopStr;
  pred R is_ringisomorph_to S means
:: QUOFIELD:def 23
  ex f being Function of R, S st f is RingIsomorphism;
  symmetry;
end;

begin :: Properties of the Field of Quotients

definition
  let I be non empty ZeroStr;
  let x, y be Element of I;
  assume
 y <> 0.I;
  func quotient(x,y) -> Element of Q.I equals
:: QUOFIELD:def 24

  [x,y];
end;

definition
  let I be non degenerated domRing-like commutative Ring;
  func canHom(I) -> Function of I, the_Field_of_Quotients(I) means
:: QUOFIELD:def 25

  for x being Element of I holds it.x = QClass.(quotient(x,1.I));
end;

theorem :: QUOFIELD:56
  for I being non degenerated domRing-like commutative Ring holds
  canHom(I) is RingHomomorphism;

theorem :: QUOFIELD:57
  for I being non degenerated domRing-like commutative Ring holds
  canHom(I) is embedding;

theorem :: QUOFIELD:58
  for I being non degenerated domRing-like commutative Ring holds I
  is_embedded_in the_Field_of_Quotients(I);

theorem :: QUOFIELD:59
  for F being non degenerated almost_left_invertible domRing-like
  commutative Ring holds F is_ringisomorph_to the_Field_of_Quotients(F);

registration
  let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) -> domRing-like right_unital
    right-distributive;
end;

theorem :: QUOFIELD:60
  for I being non degenerated domRing-like commutative Ring holds
  the_Field_of_Quotients(the_Field_of_Quotients(I)) is_ringisomorph_to
  the_Field_of_Quotients(I);

:: Universal Property of Fields of Quotients

definition
  let I, F be non empty doubleLoopStr;
  let f be Function of I, F;
  pred I has_Field_of_Quotients_Pair F,f means
:: QUOFIELD:def 26
  f is RingMonomorphism &
  for F9 being add-associative right_zeroed right_complementable Abelian
  commutative associative well-unital distributive almost_left_invertible non
  degenerated non empty doubleLoopStr for f9 being Function of I, F9 st f9 is
RingMonomorphism holds ex h being Function of F, F9 st h is RingHomomorphism &
h*f = f9 & for h9 being Function of F, F9 st h9 is RingHomomorphism & h9*f = f9
  holds h9 = h;
end;

theorem :: QUOFIELD:61
  for I being non degenerated domRing-like commutative Ring holds ex F
  being add-associative right_zeroed right_complementable Abelian commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr st ex f being Function of I, F st I
  has_Field_of_Quotients_Pair F,f;

theorem :: QUOFIELD:62
  for I being domRing-like commutative Ring for F,F9 being
  add-associative right_zeroed right_complementable Abelian commutative
  associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr for f being Function of I, F for f9 being Function of
I, F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,
  f9 holds F is_ringisomorph_to F9;