:: The correctness of the Generic Algorithms of Brown and Henrici
:: concerning Addition and Multiplication in Fraction Fields
::  by Christoph Schwarzweller
::
:: Received June 16, 1997
:: Copyright (c) 1997-2012 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 BINOP_1, VECTSP_1, XBOOLE_0, ALGSTR_0, SUBSET_1, MESFUNC1,
      RELAT_1, LATTICES, ARYTM_3, FUNCSDOM, VECTSP_2, SUPINF_2, CARD_1,
      STRUCT_0, RLVECT_1, ARYTM_1, GROUP_1, EQREL_1, TARSKI, SETFAM_1,
      MSSUBFAM, INT_2, GCD_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, STRUCT_0, ALGSTR_0, RLVECT_1,
      GROUP_1, VECTSP_2, VECTSP_1, FUNCSDOM;
 constructors BINOP_2, VECTSP_2, MONOID_0;
 registrations XBOOLE_0, SUBSET_1, MEMBERED, STRUCT_0, VECTSP_1, MONOID_0;
 requirements SUBSET, BOOLE;
 definitions VECTSP_1, VECTSP_2, XBOOLE_0;
 theorems TARSKI, WELLORD2, SUBSET_1, VECTSP_1, VECTSP_2, RLVECT_1, XBOOLE_0,
      XCMPLX_1, GROUP_1, STRUCT_0;
 schemes SUBSET_1;

begin :: Basics

reserve X,Y for set;

:: Theorems about Integral Domains

registration
  cluster commutative right_unital -> left_unital for non empty multLoopStr;
  coherence
  proof
    let R be non empty multLoopStr such that
A1: R is commutative and
A2: R is right_unital;
    let x be Element of R;
    thus (1.R)*x = x*1.R by A1,GROUP_1:def 12
      .= x by A2,VECTSP_1:def 4;
  end;
end;

registration
  cluster commutative right-distributive -> distributive for non empty
    doubleLoopStr;
  coherence
  proof
    let R be non empty doubleLoopStr such that
A1: R is commutative and
A2: R is right-distributive;
    let x,y,z be Element of R;
    thus x*(y+z) = x*y+x*z by A2,VECTSP_1:def 2;
    thus (y+z)*x = x*(y+z) by A1,GROUP_1:def 12
      .= x*y+x*z by A2,VECTSP_1:def 2
      .= y*x+x*z by A1,GROUP_1:def 12
      .= y*x+z*x by A1,GROUP_1:def 12;
  end;
  cluster commutative left-distributive -> distributive for non empty
    doubleLoopStr;
  coherence
  proof
    let R be non empty doubleLoopStr such that
A3: R is commutative and
A4: R is left-distributive;
    let x,y,z be Element of R;
    thus x*(y+z) = (y+z)*x by A3,GROUP_1:def 12
      .= y*x+z*x by A4,VECTSP_1:def 3
      .= x*y+z*x by A3,GROUP_1:def 12
      .= x*y+x*z by A3,GROUP_1:def 12;
    thus thesis by A4,VECTSP_1:def 3;
  end;
end;

registration
  cluster -> well-unital for Ring;
  coherence;
end;

registration
  cluster F_Real -> domRing-like;
  coherence
  proof
    set D = F_Real;
    hereby
      let x,y be Element of F_Real;
A1:   0.D = 0 by STRUCT_0:def 6;
      assume x*y = 0.D & x <> 0.D;
      hence y = 0.D by A1,XCMPLX_1:6;
    end;
  end;
end;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative domRing-like distributive well-unital non degenerated
    almost_left_invertible for non empty doubleLoopStr;
  existence
  proof
    take F_Real;
    thus thesis;
  end;
end;

reserve R for domRing-like commutative Ring;
reserve c for Element of R;

theorem Th1:
  for R being domRing-like commutative Ring for a,b,c being Element
  of R holds a <> 0.R implies (a * b = a * c implies b = c) & (b * a = c * a
  implies b = c)
proof
  let R be domRing-like commutative Ring;
  let a,b,c be Element of R;
  assume
A1: a <> 0.R;
  now
    assume a * b = a * c;
    then 0.R = (a * b) + (-(a * c)) by RLVECT_1:def 10
      .= (a * b) + (a *(-c)) by VECTSP_1:8
      .= a * (b + (-c)) by VECTSP_1:def 2
      .= a * (b - c) by RLVECT_1:def 11;
    then b - c = 0.R by A1,VECTSP_2:def 1;
    then c = (b - c) + c by RLVECT_1:4
      .= (b + (-c)) + c by RLVECT_1:def 11
      .= b + (c + (-c)) by RLVECT_1:def 3
      .= b + 0.R by RLVECT_1:def 10
      .= b by RLVECT_1:4;
    hence b = c;
  end;
  hence thesis;
end;

:: Definition of Divisibility

definition
  let R be non empty multMagma;
  let x,y be Element of R;
  pred x divides y means
  :Def1:
  ex z being Element of R st y = x * z;
end;

definition
  let R be right_unital non empty multLoopStr;
  let x,y be Element of R;
  redefine pred x divides y;
  reflexivity
  proof
    let A be Element of R;
    A * 1.R = A by VECTSP_1:def 4;
    hence thesis by Def1;
  end;
end;

definition
  let R be non empty multLoopStr;
  let x be Element of R;
  attr x is unital means
  :Def2:
  x divides 1.R;
end;

definition
  let R be non empty multLoopStr;
  let x,y be Element of R;
  pred x is_associated_to y means
  :Def3:
  x divides y & y divides x;
  symmetry;
end;

notation
  let R be non empty multLoopStr;
  let x,y be Element of R;
  antonym x is_not_associated_to y for x is_associated_to y;
end;

definition
  let R be well-unital non empty multLoopStr;
  let x,y be Element of R;
  redefine pred x is_associated_to y;
  reflexivity
  proof
    let a be Element of R;
    thus a divides a & a divides a;
  end;
end;

definition
  let R be domRing-like commutative Ring;
  let x,y be Element of R;
  assume
A1: y divides x;
  assume
A2: y <> 0.R;
  func x/y -> Element of R means
  :Def4:
  it * y = x;
  existence
  proof
    ex z being Element of R st x = y * z by A1,Def1;
    hence thesis;
  end;
  uniqueness by A2,Th1;
end;

:: Some Lemmata about Divisibility

theorem Th2:
  for R being associative non empty multLoopStr for a,b,c being
  Element of R holds a divides b & b divides c implies a divides c
proof
  let R be associative non empty multLoopStr;
  let A,B,C be Element of R;
  now
    assume that
A1: A divides B and
A2: B divides C;
    consider D being Element of R such that
A3: A * D = B by A1,Def1;
    consider E being Element of R such that
A4: B * E = C by A2,Def1;
    A * (D * E) = C by A3,A4,GROUP_1:def 3;
    hence thesis by Def1;
  end;
  hence thesis;
end;

theorem Th3:
  for R being commutative associative non empty multLoopStr for a
  ,b,c,d being Element of R holds (b divides a & d divides c) implies (b * d)
  divides (a * c)
proof
  let R be commutative associative non empty multLoopStr;
  let a,b,c,d be Element of R;
  assume that
A1: b divides a and
A2: d divides c;
  consider x being Element of R such that
A3: b * x = a by A1,Def1;
  consider y being Element of R such that
A4: d * y = c by A2,Def1;
  (b * d) * (y * x) = ((b * d) * y) * x by GROUP_1:def 3
    .= (b * c) * x by A4,GROUP_1:def 3
    .= a * c by A3,GROUP_1:def 3;
  hence thesis by Def1;
end;

theorem Th4:
  for R being associative non empty multLoopStr for a,b,c being
  Element of R holds a is_associated_to b & b is_associated_to c implies a
  is_associated_to c
proof
  let R be associative non empty multLoopStr;
  let A,B,C be Element of R;
  now
    assume
A1: A is_associated_to B & B is_associated_to C;
    then B divides A & C divides B by Def3;
    then
A2: C divides A by Th2;
    A divides B & B divides C by A1,Def3;
    then A divides C by Th2;
    hence thesis by A2,Def3;
  end;
  hence thesis;
end;

theorem Th5:
  for R being associative non empty multLoopStr for a,b,c being
  Element of R holds a divides b implies c * a divides c * b
proof
  let R be associative non empty multLoopStr;
  let A,B,C be Element of R;
  assume A divides B;
  then consider D being Element of R such that
A1: A * D = B by Def1;
  (C * A) * D = C * B by A1,GROUP_1:def 3;
  hence thesis by Def1;
end;

theorem Th6:
  for R being non empty multLoopStr for a,b being Element of R
  holds a divides a * b & (R is commutative implies b divides a * b)
proof
  let R be non empty multLoopStr;
  let a,b be Element of R;
  thus a divides a * b
  proof
    take b;
    thus thesis;
  end;
  assume
A1: R is commutative;
  take a;
  thus thesis by A1,GROUP_1:def 12;
end;

theorem Th7:
  for R being associative non empty multLoopStr for a,b,c being
  Element of R holds a divides b implies a divides b * c
proof
  let R be associative non empty multLoopStr;
  let a,b,c be Element of R;
  assume a divides b;
  then consider d being Element of R such that
A1: a * d = b by Def1;
  a * (d * c) = b * c by A1,GROUP_1:def 3;
  hence thesis by Def1;
end;

theorem Th8:
  for a,b being Element of R holds b divides a & b <> 0.R implies (
  a/b = 0.R iff a = 0.R)
proof
  let a,b be Element of R;
  assume that
A1: b divides a and
A2: b <> 0.R;
  hereby
    assume a/b = 0.R;
    then a = 0.R * b by A1,A2,Def4
      .= 0.R by VECTSP_1:7;
    hence a = 0.R;
  end;
  assume a = 0.R;
  then 0.R = (a/b) * b by A1,A2,Def4;
  hence thesis by A2,VECTSP_2:def 1;
end;

theorem Th9:
  for a being Element of R holds a <> 0.R implies a/a = 1.R
proof
  let A be Element of R;
  assume
A1: A <> 0.R;
  then (A/A) * A = A by Def4
    .= 1.R * A by VECTSP_1:def 8;
  hence thesis by A1,Th1;
end;

theorem Th10:
  for R being non degenerated domRing-like commutative Ring for a
  being Element of R holds a/1.R = a
proof
  let R be non degenerated domRing-like commutative Ring;
  let a be Element of R;
  set A = a/1.R;
  1.R * a = a by VECTSP_1:def 8;
  then
A1: 1.R <> 0.R & 1.R divides a by Def1;
  A = A * 1.R by VECTSP_1:def 4
    .= a by A1,Def4;
  hence thesis;
end;

theorem Th11:
  for a,b,c being Element of R holds c <> 0.R implies ( c divides
(a * b) & c divides a implies (a * b) / c = (a / c) * b) & ( c divides (a * b)
  & c divides b implies (a * b) / c = a * (b / c))
proof
  let A,B,C be Element of R;
  assume
A1: C <> 0.R;
A2: now
    set A2 = B / C;
    set A1 = (A * B) / C;
    assume C divides (A * B) & C divides B;
    then A1 * C = A * B & A2 * C = B by A1,Def4;
    then A1 * C = (A * A2) * C by GROUP_1:def 3;
    hence C divides (A * B) & C divides B implies (A * B) / C = A * (B / C) by
A1,Th1;
  end;
  now
    set A2 = A / C;
    set A1 = (A * B) / C;
    assume C divides (A * B) & C divides A;
    then A1 * C = A * B & A2 * C = A by A1,Def4;
    then A1 * C = (A2 * B) * C by GROUP_1:def 3;
    hence C divides (A * B) & C divides A implies (A * B) / C = (A / C) * B by
A1,Th1;
  end;
  hence thesis by A2;
end;

theorem Th12:
  for a,b,c being Element of R holds c <> 0.R & c divides a & c
  divides b & c divides (a + b) implies (a/c) + (b/c) = (a + b)/c
proof
  let a,b,c be Element of R;
  assume
A1: c <> 0.R;
  set e = b/c;
  set d = a/c;
  assume that
A2: c divides a & c divides b and
A3: c divides (a + b);
  d * c = a & e * c = b by A1,A2,Def4;
  then a + b = (d + e) * c by VECTSP_1:def 3;
  then (a + b)/c = (d + e) * (c/c) by A1,A3,Th11
    .= (d + e) * 1.R by A1,Th9
    .= d + e by VECTSP_1:def 4;
  hence thesis;
end;

theorem
  for a,b,c being Element of R holds c <> 0.R & c divides a & c divides
  b implies (a/c = b/c iff a = b)
proof
  let a,b,c be Element of R;
  assume
A1: c <> 0.R;
  assume that
A2: c divides a and
A3: c divides b;
  now
    assume (a/c) = (b/c);
    consider e being Element of R such that
A4: e = (b/c);
    e * c = b by A1,A3,A4,Def4;
    hence a/c = b/c implies a = b by A1,A2,A4,Def4;
  end;
  hence thesis;
end;

theorem Th14:
  for a,b,c,d being Element of R holds b <> 0.R & d <> 0.R & b
  divides a & d divides c implies (a/b) * (c/d) = (a * c) / (b * d)
proof
  let a,b,c,d be Element of R;
  assume that
A1: b <> 0.R & d <> 0.R and
A2: b divides a & d divides c;
A3: (b * d) divides (a * c) by A2,Th3;
  set z = (a * c)/(b * d);
  set y = c/d;
  set x = a/b;
A4: (b * d) <> 0.R by A1,VECTSP_2:def 1;
  x * b = a & y * d = c by A1,A2,Def4;
  then z * (b * d) = (x * b) * (y * d) by A3,A4,Def4
    .= x * (b * (y * d)) by GROUP_1:def 3
    .= x * (y * (b * d)) by GROUP_1:def 3
    .= (x * y) * (b * d) by GROUP_1:def 3;
  hence thesis by A4,Th1;
end;

theorem Th15:
  for a,b,c being Element of R holds a <> 0.R & (a * b) divides (a
  * c) implies b divides c
proof
  let A,B,C be Element of R;
  assume that
A1: A <> 0.R and
A2: (A * B) divides (A * C);
  consider D being Element of R such that
A3: (A * B) * D = A * C by A2,Def1;
  A divides (A * C) by Th6;
  then
A4: (A * C)/A = (A/A) * C by A1,Th11;
  A divides (A * (B * D)) by Th6;
  then
A5: (A * (B * D))/A = (A/A) * (B * D) by A1,Th11;
A6: A * (B * D) = A * C by A3,GROUP_1:def 3;
  B * D = 1.R * (B * D) by VECTSP_1:def 8
    .= (A/A) * C by A1,A6,A5,A4,Th9
    .= 1.R * C by A1,Th9
    .= C by VECTSP_1:def 8;
  hence thesis by Def1;
end;

theorem
  for a being Element of R holds a is_associated_to 0.R implies a = 0.R
proof
  let A be Element of R;
  assume A is_associated_to 0.R;
  then 0.R divides A by Def3;
  then ex D being Element of R st 0.R * D = A by Def1;
  hence thesis by VECTSP_1:7;
end;

theorem Th17:
  for a,b being Element of R holds a <> 0.R & a * b = a implies b = 1.R
proof
  let A,B be Element of R;
  assume that
A1: A <> 0.R and
A2: A * B = A;
  set A1 = A/A;
  A1 = 1.R & (A * B)/A = (A/A) * B by A1,A2,Th9,Th11;
  hence thesis by A2,VECTSP_1:def 8;
end;

theorem Th18:
  for a,b being Element of R holds a is_associated_to b iff ex c
  st c is unital & a * c = b
proof
A1: for a,b being Element of R holds a is_associated_to b implies ex c being
  Element of R st c is unital & a * c = b
  proof
    let A,B be Element of R;
    assume
A2: A is_associated_to B;
    then A divides B by Def3;
    then consider C being Element of R such that
A3: B = A * C by Def1;
    B divides A by A2,Def3;
    then consider D being Element of R such that
A4: A = B * D by Def1;
    now
      per cases;
      case
A5:     A <> 0.R;
        A = A * (C * D) by A3,A4,GROUP_1:def 3;
        then C * D = 1.R by A5,Th17;
        then C divides 1.R by Def1;
        then C is unital by Def2;
        hence thesis by A3;
      end;
      case
A6:     A = 0.R;
        1.R divides 1.R;
        then
A7:     1.R is unital by Def2;
        B = 0.R by A3,A6,VECTSP_1:7;
        then B = A * 1.R by A6,VECTSP_1:def 4;
        hence thesis by A7;
      end;
    end;
    hence thesis;
  end;
  for a,b being Element of R holds (ex c being Element of R st (c is
  unital & a * c = b)) implies a is_associated_to b
  proof
    let A,B be Element of R;
    (ex c st (c is unital & A * c = B)) implies A is_associated_to B
    proof
      now
        assume ex c st c is unital & A * c = B;
        then consider C being Element of R such that
A8:     C is unital and
A9:     A * C = B;
        C divides 1.R by A8,Def2;
        then consider D being Element of R such that
A10:    C * D = 1.R by Def1;
        A = A * (C * D) by A10,VECTSP_1:def 4
          .= B * D by A9,GROUP_1:def 3;
        then
A11:    B divides A by Def1;
        A divides B by A9,Def1;
        hence thesis by A11,Def3;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  hence thesis by A1;
end;

theorem Th19:
  for a,b,c being Element of R holds c <> 0.R & c * a
  is_associated_to c * b implies a is_associated_to b
proof
  let A,B,C be Element of R;
  assume that
A1: C <> 0.R and
A2: (C * A) is_associated_to (C * B);
  C * B divides C * A by A2,Def3;
  then
A3: B divides A by A1,Th15;
  (C * A) divides (C * B) by A2,Def3;
  then A divides B by A1,Th15;
  hence thesis by A3,Def3;
end;

begin

:: Definition of Ample Set

definition
  let R be non empty multLoopStr;
  let a be Element of R;
  func Class a -> Subset of R means
  :Def5:
  for b being Element of R holds b in it iff b is_associated_to a;
  existence
  proof
    set M = { b where b is Element of R: b is_associated_to a};
    now
      let B be set;
      now
        assume B in M;
        then ex B9 being Element of R st B = B9 & B9 is_associated_to a;
        hence B in M implies B in the carrier of R;
      end;
      hence B in M implies B in the carrier of R;
    end;
    then
A1: M c= the carrier of R by TARSKI:def 3;
    now
      let A be Element of R;
      A in M implies A is_associated_to a
      proof
        assume A in M;
        then ex A9 being Element of R st A = A9 & A9 is_associated_to a;
        hence thesis;
      end;
      hence A in M iff A is_associated_to a;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    defpred P[Element of R] means $1 is_associated_to a;
    let X1,X2 be Subset of R such that
A2: for y being Element of R holds y in X1 iff P[y] and
A3: for y being Element of R holds y in X2 iff P[y];
    thus X1 = X2 from SUBSET_1:sch 2(A2,A3);
  end;
end;

registration
  let R be well-unital non empty multLoopStr;
  let a be Element of R;
  cluster Class a -> non empty;
  coherence
  proof
    a is_associated_to a;
    hence thesis by Def5;
  end;
end;

theorem Th20:
  for R being associative non empty multLoopStr for a,b being
  Element of R holds Class a meets Class b implies Class a = Class b
proof
  let R be associative non empty multLoopStr;
  let a,b be Element of R;
  assume Class a /\ Class b <> {};
  then Class a meets Class b by XBOOLE_0:def 7;
  then consider Z being set such that
A1: Z in Class a and
A2: Z in Class b by XBOOLE_0:3;
  reconsider Z as Element of R by A1;
A3: Z is_associated_to b by A2,Def5;
A4: Z is_associated_to a by A1,Def5;
A5: for c being Element of R holds c in Class b implies c in Class a
  proof
    let c be Element of R;
    assume c in Class b;
    then c is_associated_to b by Def5;
    then Z is_associated_to c by A3,Th4;
    then a is_associated_to c by A4,Th4;
    hence thesis by Def5;
  end;
  for c be Element of R holds c in Class a implies c in Class b
  proof
    let c be Element of R;
    assume c in Class a;
    then c is_associated_to a by Def5;
    then Z is_associated_to c by A4,Th4;
    then b is_associated_to c by A3,Th4;
    hence thesis by Def5;
  end;
  hence thesis by A5,SUBSET_1:3;
end;

definition
  let R be non empty multLoopStr;
  func Classes R -> Subset-Family of R means
  :Def6:
  for A being Subset of R
  holds A in it iff ex a being Element of R st A = Class a;
  existence
  proof
    defpred P[set] means ex a being Element of R st $1 = Class a;
    ex F being Subset-Family of R st for A being Subset of R holds A in F
    iff P[A] from SUBSET_1:sch 3;
    hence thesis;
  end;
  uniqueness
  proof
    defpred P[set] means ex a being Element of R st $1 = Class a;
    let F1,F2 be Subset-Family of R;
    assume
A1: for A being Subset of R holds A in F1 iff P[A];
    assume
A2: for A being Subset of R holds A in F2 iff P[A];
    thus thesis from SUBSET_1:sch 4(A1,A2);
  end;
end;

registration
  let R be non empty multLoopStr;
  cluster Classes R -> non empty;
  coherence
  proof
    Class 1.R in Classes R by Def6;
    hence thesis;
  end;
end;

theorem Th21:
  for R being well-unital non empty multLoopStr for X being
  Subset of R holds X in Classes R implies X is non empty
proof
  let R be well-unital non empty multLoopStr;
  let X be Subset of R;
  assume X in Classes R;
  then ex a being Element of R st X = Class a by Def6;
  hence thesis;
end;

definition
  let R be associative well-unital non empty multLoopStr;
  mode Am of R -> non empty Subset of R means
    :Def7:
    (for a being Element of R
ex z being Element of it st z is_associated_to a) & for x,y being Element of it
    holds x <> y implies x is_not_associated_to y;
  existence
  proof
    now
      let R be associative well-unital non empty multLoopStr;
      reconsider M = Classes R as non empty set;
A1:   for X st X in M holds X <> {}
      proof
        let X be set;
        assume X in M;
        then ex A being Element of R st X = Class A by Def6;
        hence thesis;
      end;
      for X,Y st X in M & Y in M & X <> Y holds X misses Y
      proof
        let X,Y be set such that
A2:     X in M & Y in M and
A3:     X <> Y;
        assume
A4:     X meets Y;
        (ex A being Element of R st X = Class A )& ex B being Element of R
        st Y = Class B by A2,Def6;
        hence contradiction by A3,A4,Th20;
      end;
      then consider AmpS9 being set such that
A5:   for X st X in M ex x being set st AmpS9 /\ X = {x} by A1,WELLORD2:18;
      AmpS9 is non empty
      proof
        Class 1.R in M by Def6;
        then ex x being set st AmpS9 /\ Class 1.R = {x} by A5;
        hence thesis;
      end;
      then reconsider AmpS9 as non empty set;
      set AmpS = { x where x is Element of AmpS9: ex X being non empty Subset
      of R st X in M & AmpS9 /\ X = { x }};
A6:   AmpS is non empty Subset of R
      proof
        AmpS is non empty
        proof
A7:       Class 1.R in M by Def6;
          then consider x being set such that
A8:       AmpS9 /\ Class 1.R = {x} by A5;
          x in {x} by TARSKI:def 1;
          then x in AmpS9 by A8,XBOOLE_0:def 4;
          then x in AmpS by A7,A8;
          hence thesis;
        end;
        then reconsider AmpS as non empty set;
        now
          let A be set;
          now

            assume A in AmpS;
            then consider x being Element of AmpS9 such that
A9:         A = x & ex X being non empty Subset of R st X in M &
            AmpS9 /\ X = {x};
            x in {x} by TARSKI:def 1;
            hence A in AmpS implies A in the carrier of R by A9;
          end;
          hence A in AmpS implies A in the carrier of R;
        end;
        hence thesis by TARSKI:def 3;
      end;
A10:  for X being Element of M holds ex z being Element of AmpS st AmpS
      /\ X = {z}
      proof
        let X be Element of M;
        consider x being set such that
A11:    AmpS9 /\ X = {x} by A5;
        X in Classes R;
        then
A12:    X is non empty Subset of R by Th21;
A13:    x in {x} by TARSKI:def 1;
        then x in AmpS9 by A11,XBOOLE_0:def 4;
        then
A14:    x in AmpS by A11,A12;
A15:    x in X by A11,A13,XBOOLE_0:def 4;
        now
          let y be set;
A16:      now
            assume
A17:        y in AmpS /\ X;
            then y in AmpS by XBOOLE_0:def 4;
            then
A18:        ex zz being Element of AmpS9 st y = zz & ex X being non empty
            Subset of R st X in M & AmpS9 /\ X = {zz};
            y in X by A17,XBOOLE_0:def 4;
            hence y in AmpS /\ X implies y in {x} by A11,A18,XBOOLE_0:def 4;
          end;
          now
            assume y in {x};
            then y = x by TARSKI:def 1;
            hence y in {x} implies y in AmpS /\ X by A15,A14,XBOOLE_0:def 4;
          end;
          hence y in {x} iff y in AmpS /\ X by A16;
        end;
        then AmpS /\ X = {x} by TARSKI:1;
        hence thesis by A14;
      end;
      reconsider AmpS as non empty Subset of R by A6;
A19:  for x,y being Element of AmpS holds x <> y implies x
      is_not_associated_to y
      proof
        let x,y be Element of AmpS;
        assume
A20:    x <> y;
        x is_associated_to x;
        then x in Class x by Def5;
        then
A21:    x in AmpS /\ Class x by XBOOLE_0:def 4;
        Class x in M by Def6;
        then consider z being Element of AmpS such that
A22:    AmpS /\ Class x = {z} by A10;
        assume x is_associated_to y;
        then y in Class x by Def5;
        then y in AmpS /\ Class x by XBOOLE_0:def 4;
        then y = z by A22,TARSKI:def 1;
        hence thesis by A20,A21,A22,TARSKI:def 1;
      end;
      for a being Element of R ex z being Element of AmpS st z
      is_associated_to a
      proof
        let a be Element of R;
        reconsider N = Class a as Element of M by Def6;
        consider z being Element of AmpS such that
A23:    AmpS /\ N = {z} by A10;
        z in {z} by TARSKI:def 1;
        then z in Class a by A23,XBOOLE_0:def 4;
        then z is_associated_to a by Def5;
        hence thesis;
      end;
      hence ex s being non empty Subset of R st (for a being Element of R ex z
being Element of s st z is_associated_to a) & for x,y being Element of s holds
      x <> y implies x is_not_associated_to y by A19;
    end;
    hence thesis;
  end;
end;

definition
  let R be associative well-unital non empty multLoopStr;
  mode AmpleSet of R -> non empty Subset of R means
    :Def8:
    it is Am of R & 1.R in it;
  existence
  proof
    now
      let A be Am of R;
      consider x being Element of A such that
A1:   x is_associated_to 1.R by Def7;
      set A9 = { z where z is Element of A : z <> x } \/ {1.R};
      1.R in {1.R} by TARSKI:def 1;
      then
A2:   1.R in A9 by XBOOLE_0:def 3;
      reconsider A9 as non empty set;
A3:   for x being Element of A9 holds x = 1.R or x in A
      proof
        let y be Element of A9;
        now
          per cases by XBOOLE_0:def 3;
          case
            y in {z where z is Element of A: z <> x};
            then ex zz being Element of A st y = zz & zz <> x;
            hence thesis;
          end;
          case
            y in {1.R};
            hence thesis by TARSKI:def 1;
          end;
        end;
        hence thesis;
      end;
      now
        let x be set;
        now
          assume
A4:       x in A9;
          x in the carrier of R
          proof
            now
              per cases by A3,A4;
              case
                x = 1.R;
                hence thesis;
              end;
              case
                x in A;
                hence thesis;
              end;
            end;
            hence thesis;
          end;
          hence x in A9 implies x in the carrier of R;
        end;
        hence x in A9 implies x in the carrier of R;
      end;
      then reconsider A9 as non empty Subset of R by TARSKI:def 3;
A5:   for z,y being Element of A9 holds z <> y implies z is_not_associated_to y
      proof
        let z,y be Element of A9;
        assume
A6:     z <> y;
        now
          per cases;
          case
            z = 1.R & y = 1.R;
            hence thesis by A6;
          end;
          case
A7:         z = 1.R & y <> 1.R;
            assume z is_associated_to y;
            not y in {1.R} by A7,TARSKI:def 1;
            then y in {zz where zz is Element of A: zz <> x} by XBOOLE_0:def 3;
            then ex zz being Element of A st y = zz & zz <> x;
            hence thesis by A1,A7,Def7,Th4;
          end;
          case
A8:         z <> 1.R & y = 1.R;
            assume z is_associated_to y;
            not z in {1.R} by A8,TARSKI:def 1;
            then z in {zz where zz is Element of A: zz <> x} by XBOOLE_0:def 3;
            then ex zz being Element of A st z = zz & zz <> x;
            hence thesis by A1,A8,Def7,Th4;
          end;
          case
            z <> 1.R & y <> 1.R;
            then z in A & y in A by A3;
            hence thesis by A6,Def7;
          end;
        end;
        hence thesis;
      end;
      for a being Element of R ex z being Element of A9 st z is_associated_to a
      proof
        let a be Element of R;
        now
          per cases;
          case
            a is_associated_to 1.R;
            hence thesis by A2;
          end;
          case
A9:         a is_not_associated_to 1.R;
            consider z being Element of A such that
A10:        z is_associated_to a by Def7;
            z <> x by A1,A9,A10,Th4;
            then z in {zz where zz is Element of A : zz <> x};
            then z in A9 by XBOOLE_0:def 3;
            hence thesis by A10;
          end;
        end;
        hence thesis;
      end;
      then A9 is Am of R by A5,Def7;
      hence thesis by A2;
    end;
    hence thesis;
  end;
end;

theorem Th22:
  for R being associative well-unital non empty multLoopStr for
  Amp being AmpleSet of R holds (1.R in Amp) & (for a being Element of R ex z
  being Element of Amp st z is_associated_to a) & (for x,y being Element of Amp
  holds x <> y implies x is_not_associated_to y)
proof
  let R be associative well-unital non empty multLoopStr;
  let Amp be AmpleSet of R;
  Amp is Am of R by Def8;
  hence thesis by Def7,Def8;
end;

theorem
  for R being associative well-unital non empty multLoopStr for Amp
  being AmpleSet of R for x,y being Element of Amp holds x is_associated_to y
  implies x = y by Th22;

theorem Th24:
  for Amp being AmpleSet of R holds 0.R is Element of Amp
proof
  let Amp be AmpleSet of R;
  consider A being Element of Amp such that
A1: A is_associated_to 0.R by Th22;
  0.R divides A by A1,Def3;
  then ex D being Element of R st 0.R * D = A by Def1;
  hence thesis by VECTSP_1:7;
end;

:: Definition of Normalform

definition
  let R be associative well-unital non empty multLoopStr;
  let Amp be AmpleSet of R;
  let x be Element of R;
  func NF(x,Amp) -> Element of R means
  :Def9:
  it in Amp & it is_associated_to x;
  existence
  proof
    now
      let Amp be AmpleSet of R;
      let x be Element of R;
      ex z being Element of Amp st z is_associated_to x by Th22;
      hence ex zz being Element of R st zz in Amp & zz is_associated_to x;
    end;
    hence thesis;
  end;
  uniqueness by Th4,Th22;
end;

theorem Th25:
  for Amp being AmpleSet of R holds NF(0.R,Amp) = 0.R & NF(1.R,Amp ) = 1.R
proof
  let Amp be AmpleSet of R;
  1.R in Amp & 0.R is Element of Amp by Def8,Th24;
  hence thesis by Def9;
end;

theorem
  for Amp being AmpleSet of R for a being Element of R holds a in Amp
  iff a = NF(a,Amp) by Def9;

:: Definition of multiplicative AmpleSet

definition
  let R be associative well-unital non empty multLoopStr;
  let Amp be AmpleSet of R;
  attr Amp is multiplicative means
  :Def10:
  for x,y being Element of Amp holds x * y in Amp;
end;

theorem Th27:
  for Amp being AmpleSet of R holds Amp is multiplicative implies
  for x,y being Element of Amp holds y divides x & y <> 0.R implies x/y in Amp
proof
  let Amp be AmpleSet of R;
  assume
A1: Amp is multiplicative;
  let x,y be Element of Amp;
  assume that
A2: y divides x and
A3: y <> 0.R;
  now
    per cases;
    case
A4:   x <> 0.R;
      set d = x/y;
      consider d9 being Element of Amp such that
A5:   d9 is_associated_to d by Th22;
      consider u being Element of R such that
A6:   u is unital and
A7:   d * u = d9 by A5,Th18;
      x = y * d by A2,A3,Def4;
      then
A8:   u * x = y * d9 by A7,GROUP_1:def 3;
A9:   x is_associated_to u * x
      proof
        u divides 1.R by A6,Def2;
        then consider e being Element of R such that
A10:    u * e = 1.R by Def1;
        x divides x;
        then
A11:    x divides u * x by Th7;
        (u * x) * e = (e * u) * x by GROUP_1:def 3
          .= x by A10,VECTSP_1:def 8;
        then u * x divides x by Def1;
        hence thesis by A11,Def3;
      end;
A12:  y * d9 in Amp by A1,Def10;
      1.R * x = x by VECTSP_1:def 8
        .= u * x by A8,A12,A9,Th22;
      then u = 1.R by A4,Th1;
      then d9 = d by A7,VECTSP_1:def 4;
      hence thesis;
    end;
    case
A13:  x = 0.R;
      set d = x/y;
      x = y * d by A2,A3,Def4;
      then
A14:  d = 0.R by A3,A13,VECTSP_2:def 1;
      0.R is Element of Amp by Th24;
      hence thesis by A14;
    end;
  end;
  hence thesis;
end;

begin

:: Definition of GCD-Domain

definition
  let R be non empty multLoopStr;
  attr R is gcd-like means
  :Def11:
  for x,y being Element of R ex z being
  Element of R st z divides x & z divides y & for zz being Element of R st zz
  divides x & zz divides y holds zz divides z;
end;

Lm1: now
  let F be Field;
  let x,y be Element of F;
  now
    per cases;
    case
A1:   x <> 0.F & y <> 0.F;
A2:   for zz being Element of F st zz divides x & zz divides y holds zz
      divides (1_F)
      proof
        let zz be Element of F;
        assume that
A3:     zz divides x and
        zz divides y;
        now
          per cases;
          case
            zz <> 0.F;
            then ex zz9 being Element of F st zz9 * zz = (1_F) by
VECTSP_1:def 9;
            hence thesis by Def1;
          end;
          case
A4:         zz = 0.F;
            assume zz divides x;
            then ex d being Element of F st zz * d = x by Def1;
            hence thesis by A1,A4,VECTSP_1:7;
          end;
        end;
        hence thesis by A3;
      end;
      y = (1_F) * y by VECTSP_1:def 6;
      then
A5:   (1_F) divides y by Def1;
      x = (1_F) * x by VECTSP_1:def 6;
      then (1_F) divides x by Def1;
      hence
      ex z being Element of F st z divides x & z divides y & for zz being
      Element of F st zz divides x & zz divides y holds zz divides z by A5,A2;
    end;
    case
A6:   x = 0.F;
      y * 0.F = 0.F by VECTSP_1:7;
      then
A7:   y divides 0.F by Def1;
      for z being Element of F st z divides 0.F & z divides y holds z
      divides y;
      hence
      ex z being Element of F st z divides x & z divides y & for zz being
      Element of F st zz divides x & zz divides y holds zz divides z by A6,A7;
    end;
    case
A8:   y = 0.F;
      x * 0.F = 0.F by VECTSP_1:7;
      then
A9:   x divides 0.F by Def1;
      for z being Element of F st z divides x & z divides 0.F holds z
      divides x;
      hence
      ex z being Element of F st z divides x & z divides y & for zz being
      Element of F st zz divides x & zz divides y holds zz divides z by A8,A9;
    end;
  end;
  hence ex z being Element of F st z divides x & z divides y & for zz being
  Element of F st zz divides x & zz divides y holds zz divides z;
end;

registration
  cluster gcd-like for domRing;
  existence
  proof
    set F = the strict Field;
    reconsider F as comRing;
    reconsider F as domRing by VECTSP_2:1;
    for x,y be Element of F holds ex z being Element of F st z divides x &
z divides y & for zz being Element of F st zz divides x & zz divides y holds zz
    divides z by Lm1;
    then F is gcd-like by Def11;
    hence thesis;
  end;
end;

registration
  cluster gcd-like associative commutative well-unital for
non empty multLoopStr;
  existence
  proof
    set F = the strict Field;
    for x,y be Element of F holds ex z being Element of F st z divides x &
z divides y & for zz being Element of F st zz divides x & zz divides y holds zz
    divides z by Lm1;
    then F is gcd-like by Def11;
    hence thesis;
  end;
end;

registration
  cluster gcd-like associative commutative well-unital for non empty
    multLoopStr_0;
  existence
  proof
    set F = the strict Field;
    for x,y be Element of F holds ex z being Element of F st z divides x &
z divides y & for zz being Element of F st zz divides x & zz divides y holds zz
    divides z by Lm1;
    then F is gcd-like by Def11;
    hence thesis;
  end;
end;

registration
  cluster -> gcd-like for almost_left_invertible add-associative right_zeroed
    right_complementable left_unital well-unital left-distributive
    right-distributive commutative non empty doubleLoopStr;
  coherence
  proof
    let F be almost_left_invertible add-associative right_zeroed
    right_complementable left_unital well-unital left-distributive
    right-distributive commutative non empty doubleLoopStr;
    let x,y be Element of F;
    now
      per cases;
      case
A1:     x <> 0.F & y <> 0.F;
A2:     for zz being Element of F st zz divides x & zz divides y holds zz
        divides 1_F
        proof
          let zz be Element of F;
          assume that
A3:       zz divides x and
          zz divides y;
          now
            per cases;
            case
              zz <> 0.F;
              then ex zz9 being Element of F st zz9 * zz = 1_F by
VECTSP_1:def 9;
              hence thesis by Def1;
            end;
            case
A4:           zz = 0.F;
              assume zz divides x;
              then ex d being Element of F st zz * d = x by Def1;
              hence thesis by A1,A4,VECTSP_1:7;
            end;
          end;
          hence thesis by A3;
        end;
        y = 1_F * y by VECTSP_1:def 8;
        then
A5:     1_F divides y by Def1;
        x = 1_F * x by VECTSP_1:def 8;
        then 1_F divides x by Def1;
        hence ex z being Element of F st z divides x & z divides y & for zz
being Element of F st zz divides x & zz divides y holds zz divides z by A5,A2;
      end;
      case
A6:     x = 0.F;
        y * 0.F = 0.F by VECTSP_1:6;
        then
A7:     y divides 0.F by Def1;
        for z being Element of F st z divides 0.F & z divides y holds z
        divides y;
        hence ex z being Element of F st z divides x & z divides y & for zz
being Element of F st zz divides x & zz divides y holds zz divides z by A6,A7;
      end;
      case
A8:     y = 0.F;
        x * 0.F = 0.F by VECTSP_1:6;
        then
A9:     x divides 0.F by Def1;
        for z being Element of F st z divides x & z divides 0.F holds z
        divides x;
        hence ex z being Element of F st z divides x & z divides y & for zz
being Element of F st zz divides x & zz divides y holds zz divides z by A8,A9;
      end;
    end;
    hence thesis;
  end;
end;

registration
  cluster gcd-like associative commutative well-unital domRing-like unital
    distributive non degenerated Abelian add-associative right_zeroed
    right_complementable for non empty doubleLoopStr;
  existence
  proof
    take F_Real;
    thus thesis;
  end;
end;

definition
  mode gcdDomain is gcd-like domRing-like non degenerated commutative Ring;
end;

definition
  let R be gcd-like associative well-unital non empty multLoopStr;
  let Amp be AmpleSet of R;
  let x,y be Element of R;
  func gcd(x,y,Amp) -> Element of R means
  :Def12:
  it in Amp & it divides x &
  it divides y & for z being Element of R st z divides x & z divides y holds z
  divides it;
  existence
  proof
    consider u being Element of R such that
A1: u divides x & u divides y and
A2: for zz being Element of R st zz divides x & zz divides y holds zz
    divides u by Def11;
    consider z being Element of Amp such that
A3: z is_associated_to u by Th22;
A4: for zz being Element of R st zz divides x & zz divides y holds zz divides z
    proof
      let zz be Element of R;
      assume zz divides x & zz divides y;
      then
A5:   zz divides u by A2;
      u divides z by A3,Def3;
      hence thesis by A5,Th2;
    end;
    z divides u by A3,Def3;
    then z divides x & z divides y by A1,Th2;
    hence thesis by A4;
  end;
  uniqueness
  proof
    now
      let z1 be Element of R such that
A6:   z1 in Amp and
A7:   z1 divides x & z1 divides y & for z being Element of R st z
      divides x & z divides y holds z divides z1;
      let z2 be Element of R such that
A8:   z2 in Amp and
A9:   z2 divides x & z2 divides y & for z being Element of R st z
      divides x & z divides y holds z divides z2;
      z1 divides z2 & z2 divides z1 by A7,A9;
      then z1 is_associated_to z2 by Def3;
      hence z1 = z2 by A6,A8,Th22;
    end;
    hence thesis;
  end;
end;

reserve R for gcdDomain;

:: Lemmata about GCD

theorem Th28:
  for Amp being AmpleSet of R for a,b,c being Element of R holds c
  divides gcd(a,b,Amp) implies c divides a & c divides b
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
  assume C divides gcd(A,B,Amp);
  then consider D being Element of R such that
A1: C * D = gcd(A,B,Amp) by Def1;
  gcd(A,B,Amp) divides A by Def12;
  then consider E being Element of R such that
A2: gcd(A,B,Amp) * E = A by Def1;
A3: C * (D * E) = A by A1,A2,GROUP_1:def 3;
  gcd(A,B,Amp) divides B by Def12;
  then consider E being Element of R such that
A4: gcd(A,B,Amp) * E = B by Def1;
  C * (D * E) = B by A1,A4,GROUP_1:def 3;
  hence thesis by A3,Def1;
end;

theorem Th29:
  for Amp being AmpleSet of R for a,b being Element of R holds gcd
  (a,b,Amp) = gcd(b,a,Amp)
proof
  let Amp be AmpleSet of R;
  let A,B be Element of R;
  set D = gcd(A,B,Amp);
A1: D divides A & for z being Element of R st z divides B & z divides A
  holds z divides D by Def12;
  D in Amp & D divides B by Def12;
  hence thesis by A1,Def12;
end;

theorem Th30:
  for Amp being AmpleSet of R for a being Element of R holds gcd(a
  ,0.R,Amp) = NF(a,Amp) & gcd(0.R,a,Amp) = NF(a,Amp)
proof
  let Amp be AmpleSet of R;
  let A be Element of R;
A1: NF(A,Amp) in Amp by Def9;
  NF(A,Amp) * 0.R = 0.R by VECTSP_1:6;
  then
A2: NF(A,Amp) divides 0.R by Def1;
A3: NF(A,Amp)is_associated_to A by Def9;
A4: for z being Element of R st z divides A & z divides 0.R holds z divides
  NF(A,Amp)
  proof
    let z be Element of R;
    assume that
A5: z divides A and
    z divides 0.R;
    A divides NF(A,Amp) by A3,Def3;
    hence thesis by A5,Th2;
  end;
  NF(A,Amp) divides A by A3,Def3;
  then gcd(A,0.R,Amp) = NF(A,Amp) by A2,A4,A1,Def12;
  hence thesis by Th29;
end;

theorem Th31:
  for Amp being AmpleSet of R holds gcd(0.R,0.R,Amp) = 0.R
proof
  let Amp be AmpleSet of R;
  gcd(0.R,0.R,Amp) = NF(0.R,Amp) by Th30;
  hence thesis by Th25;
end;

theorem Th32:
  for Amp being AmpleSet of R for a being Element of R holds gcd(a
  ,1.R,Amp) = 1.R & gcd(1.R,a,Amp) = 1.R
proof
  let Amp be AmpleSet of R;
  let A be Element of R;
  1.R * A = A by VECTSP_1:def 8;
  then
A1: 1.R divides A by Def1;
  1.R in Amp & for z being Element of R st z divides A & z divides 1.R
  holds z divides 1.R by Def8;
  then gcd(A,1.R,Amp) = 1.R by A1,Def12;
  hence thesis by Th29;
end;

theorem Th33:
  for Amp being AmpleSet of R for a,b being Element of R holds gcd
  (a,b,Amp) = 0.R iff a = 0.R & b = 0.R
proof
  let Amp be AmpleSet of R;
  let A,B be Element of R;
A1: now
    assume
A2: gcd(A,B,Amp) = 0.R;
    then 0.R divides B by Def12;
    then
A3: ex E being Element of R st 0.R * E = B by Def1;
    0.R divides A by A2,Def12;
    then ex D being Element of R st 0.R * D = A by Def1;
    hence gcd(A,B,Amp) = 0.R implies A = 0.R & B = 0.R by A3,VECTSP_1:7;
  end;
  A = 0.R & B = 0.R implies gcd(A,B,Amp) = 0.R
  proof
    assume that
A4: A = 0.R and
A5: B = 0.R;
    gcd(A,B,Amp) = NF(A,Amp) by A5,Th30;
    hence thesis by A4,Th25;
  end;
  hence thesis by A1;
end;

theorem Th34:
  for Amp being AmpleSet of R for a,b,c being Element of R holds b
is_associated_to c implies gcd(a,b,Amp) is_associated_to gcd(a,c,Amp) & gcd(b,a
  ,Amp) is_associated_to gcd(c,a,Amp)
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
A1: gcd(A,B,Amp) divides B by Def12;
A2: gcd(A,B,Amp) divides A by Def12;
A3: gcd(A,C,Amp) divides A by Def12;
A4: gcd(A,C,Amp) divides C by Def12;
A5: gcd(A,B,Amp) = gcd(B,A,Amp) by Th29;
  assume
A6: B is_associated_to C;
  then C divides B by Def3;
  then gcd(A,C,Amp) divides B by A4,Th2;
  then
A7: gcd(A,C,Amp) divides gcd(A,B,Amp) by A3,Def12;
  B divides C by A6,Def3;
  then gcd(A,B,Amp) divides C by A1,Th2;
  then gcd(A,B,Amp) divides gcd(A,C,Amp) by A2,Def12;
  then gcd(A,B,Amp) is_associated_to gcd(A,C,Amp) by A7,Def3;
  hence thesis by A5,Th29;
end;

:: Main Theorems

theorem Th35:
  for Amp being AmpleSet of R for a,b,c being Element of R holds
  gcd(gcd(a,b,Amp),c,Amp) = gcd(a,gcd(b,c,Amp),Amp)
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
  set D = gcd(gcd(A,B,Amp),C,Amp);
  set E = gcd(A,gcd(B,C,Amp),Amp);
A1: D divides C by Def12;
A2: E divides A by Def12;
A3: E divides gcd(B,C,Amp) by Def12;
  then
A4: E divides C by Th28;
  E divides B by A3,Th28;
  then E divides gcd(A,B,Amp) by A2,Def12;
  then
A5: E divides D by A4,Def12;
A6: D is Element of Amp & E is Element of Amp by Def12;
A7: D divides gcd(A,B,Amp) by Def12;
  then
A8: D divides A by Th28;
  D divides B by A7,Th28;
  then D divides gcd(B,C,Amp) by A1,Def12;
  then D divides E by A8,Def12;
  then D is_associated_to E by A5,Def3;
  hence thesis by A6,Th22;
end;

theorem Th36:
  for Amp being AmpleSet of R for a,b,c being Element of R holds
  gcd(a * c,b * c,Amp) is_associated_to (c * gcd(a,b,Amp))
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
  now
    per cases;
    case
A1:   C <> 0.R;
      set D = gcd(A,B,Amp);
      now
        per cases;
        case
A2:       D <> 0.R;
          set E = gcd((A * C),(B * C),Amp);
A3:       E divides B * C by Def12;
          D divides B by Def12;
          then
A4:       C * D divides B * C by Th5;
          D divides A by Def12;
          then C * D divides A * C by Th5;
          then C * D divides gcd((A * C),(B * C),Amp) by A4,Def12;
          then consider F being Element of R such that
A5:       E = (C * D) * F by Def1;
A6:       E divides A * C by Def12;
          (D * F) divides A & (D * F) divides B
          proof
            consider G being Element of R such that
A7:         ((C * D) * F) * G = A * C by A5,A6,Def1;
            (C * (D * F)) * G = C * A by A7,GROUP_1:def 3;
            then
A8:         (C * (D * F)) divides C * A by Def1;
            consider G being Element of R such that
A9:         ((C * D) * F) * G = B * C by A5,A3,Def1;
            (C * (D * F)) * G = C * B by A9,GROUP_1:def 3;
            then (C * (D * F)) divides C * B by Def1;
            hence thesis by A1,A8,Th15;
          end;
          then
A10:      D * F divides D by Def12;
          D = D * 1.R by VECTSP_1:def 4;
          then F divides 1.R by A2,A10,Th15;
          then F is unital by Def2;
          hence thesis by A5,Th18;
        end;
        case
A11:      D = 0.R;
          then
A12:      C * gcd(A,B,Amp) = 0.R by VECTSP_1:7;
          A = 0.R & B = 0.R by A11,Th33;
          then gcd((A * C),(B * C),Amp) = gcd(0.R,(0.R * C),Amp) by VECTSP_1:7
            .= gcd(0.R,0.R,Amp) by VECTSP_1:7
            .= C * gcd(A,B,Amp) by A12,Th31;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    case
A13:  C = 0.R;
      then A * C = 0.R & B * C = 0.R by VECTSP_1:7;
      then gcd((A * C),(B * C),Amp) = 0.R by Th31
        .= C * gcd(A,B,Amp) by A13,VECTSP_1:7;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th37:
  for Amp being AmpleSet of R for a,b,c being Element of R holds
  gcd(a,b,Amp) = 1.R implies gcd(a,(b * c),Amp) = gcd(a,c,Amp)
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
  assume gcd(A,B,Amp) = 1.R;
  then
A1: C * (gcd(A,B,Amp)) = C by VECTSP_1:def 4;
  gcd((A * C),(B * C),Amp) is_associated_to (C * gcd(A,B,Amp)) by Th36;
  then gcd(A,C,Amp) is_associated_to gcd(A,gcd((A * C),(B * C),Amp),Amp) by A1
,Th34;
  then
A2: gcd(A,C,Amp) is_associated_to gcd(gcd(A,(A * C),Amp),(B * C),Amp) by Th35;
A3: A * gcd(1.R,C,Amp) = A * 1.R by Th32
    .= A by VECTSP_1:def 4;
  gcd((A * 1.R),(A * C),Amp) is_associated_to (A * gcd(1.R,C,Amp)) by Th36;
  then gcd(A,(A * C),Amp) is_associated_to A by A3,VECTSP_1:def 4;
  then
A4: gcd(gcd(A,(A * C),Amp),(B * C),Amp) is_associated_to gcd(A,(B * C),Amp)
  by Th34;
  gcd(A,(B * C),Amp) is Element of Amp & gcd(A,C,Amp) is Element of Amp
  by Def12;
  hence thesis by A2,A4,Th4,Th22;
end;

theorem Th38:
  for Amp being AmpleSet of R for a,b,c being Element of R holds c
  = gcd(a,b,Amp) & c <> 0.R implies gcd((a/c),(b/c),Amp) = 1.R
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
  assume that
A1: C = gcd(A,B,Amp) and
A2: C <> 0.R;
  set A1 = A/C;
  C divides A by A1,Def12;
  then
A3: A1 * C = A by A2,Def4;
  set B1 = B/C;
A4: gcd((A1 * C),(B1 * C),Amp) is_associated_to (C * gcd(A1,B1,Amp)) by Th36;
A5: gcd(A1,B1,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
  C divides B by A1,Def12;
  then gcd(A,B,Amp) = gcd((A1 * C),(B1 * C),Amp) by A2,A3,Def4;
  then (C * 1.R) is_associated_to (C * gcd(A1,B1,Amp)) by A1,A4,VECTSP_1:def 4
;
  hence thesis by A2,A5,Th19,Th22;
end;

theorem Th39:
  for Amp being AmpleSet of R for a,b,c being Element of R holds
  gcd((a + (b * c)),c,Amp) = gcd(a,c,Amp)
proof
  let Amp be AmpleSet of R;
  let A,B,C be Element of R;
  set D = gcd(A,C,Amp);
  D divides A by Def12;
  then consider E being Element of R such that
A1: D * E = A by Def1;
A2: D divides C by Def12;
  then consider F being Element of R such that
A3: D * F = C by Def1;
A4: for z being Element of R st z divides (A + (B * C)) & z divides C holds
  z divides D
  proof
    let Z be Element of R;
    assume that
A5: Z divides (A + (B * C)) and
A6: Z divides C;
    consider X being Element of R such that
A7: Z * X = C by A6,Def1;
    consider Y being Element of R such that
A8: Z * Y = A + (B * C) by A5,Def1;
    Z * (Y + (-(B * X))) = (Z * Y) + (Z * (-(B * X))) by VECTSP_1:def 2
      .= (Z * Y) + (-(Z * (X * B))) by VECTSP_1:8
      .= (A + (B * C)) + (-(C * B)) by A7,A8,GROUP_1:def 3
      .= A + ((B * C) + (-(C * B))) by RLVECT_1:def 3
      .= A + 0.R by RLVECT_1:def 10
      .= A by RLVECT_1:4;
    then Z divides A by Def1;
    hence thesis by A6,Def12;
  end;
  D * (E + (F * B)) = (D * E) + (D * (F * B)) by VECTSP_1:def 2
    .= A + (B * C) by A1,A3,GROUP_1:def 3;
  then
A9: D divides (A + (B * C)) by Def1;
  D is Element of Amp by Def12;
  hence thesis by A2,A9,A4,Def12;
end;

begin

:: Brown & Henrici

::$N Brown Theorem
theorem Th40:
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R
holds gcd(r1,r2,Amp) = 1.R & gcd(s1,s2,Amp) = 1.R & r2 <> 0.R implies gcd(((r1
* (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))), (r2 * (s2/gcd(r2,s2,Amp))
),Amp) = gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))), gcd(r2,
  s2,Amp),Amp)
proof
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: gcd(r1,r2,Amp) = 1.R and
A2: gcd(s1,s2,Amp) = 1.R and
A3: r2 <> 0.R;
  set d = gcd(r2,s2,Amp);
  set r = r2/d;
  set s = s2/d;
A4: d <> 0.R by A3,Th33;
  then
A5: gcd(r,s,Amp) = 1.R by Th38;
A6: d divides s2 by Def12;
  gcd(s,s1,Amp) = 1.R
  proof
    gcd(s,s1,Amp) divides s by Def12;
    then consider e being Element of R such that
A7: gcd(s,s1,Amp) * e = s by Def1;
    gcd(s,s1,Amp) * (e * d) = s * d by A7,GROUP_1:def 3
      .= s2 by A6,A4,Def4;
    then
A8: gcd(s,s1,Amp) divides s2 by Def1;
A9: gcd(s,s1,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
    1.R * gcd(s,s1,Amp) = gcd(s,s1,Amp) by VECTSP_1:def 8;
    then
A10: 1.R divides gcd(s,s1,Amp) by Def1;
    gcd(s,s1,Amp) divides s1 by Def12;
    then gcd(s,s1,Amp) divides gcd(s1,s2,Amp) by A8,Def12;
    then gcd(s,s1,Amp) is_associated_to 1.R by A2,A10,Def3;
    hence thesis by A9,Th22;
  end;
  then
A11: gcd(s,(s1 * r),Amp) = gcd(s,r,Amp) by Th37;
  gcd(((r1 * s) + (s1 * r)),s,Amp) = gcd((s1 * r),s,Amp) by Th39;
  then
A12: gcd(((r1 * s) + (s1 * r)),s,Amp) = gcd(s,(s1 * r),Amp) by Th29
    .= 1.R by A11,A5,Th29;
A13: d divides (d * r2) by Th6;
A14: d divides r2 by Def12;
  gcd(r,r1,Amp) = 1.R
  proof
    gcd(r,r1,Amp) divides r by Def12;
    then consider e being Element of R such that
A15: gcd(r,r1,Amp) * e = r by Def1;
    gcd(r,r1,Amp) * (e * d) = r * d by A15,GROUP_1:def 3
      .= r2 by A14,A4,Def4;
    then
A16: gcd(r,r1,Amp) divides r2 by Def1;
A17: gcd(r,r1,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
    1.R * gcd(r,r1,Amp) = gcd(r,r1,Amp) by VECTSP_1:def 8;
    then
A18: 1.R divides gcd(r,r1,Amp) by Def1;
    gcd(r,r1,Amp) divides r1 by Def12;
    then gcd(r,r1,Amp) divides gcd(r1,r2,Amp) by A16,Def12;
    then gcd(r,r1,Amp) is_associated_to 1.R by A1,A18,Def3;
    hence thesis by A17,Th22;
  end;
  then
A19: gcd(r,(r1 * s),Amp) = gcd(r,s,Amp) by Th37;
A20: gcd(((r1 * s) + (s1 * r)),r,Amp) = gcd((r1 * s),r,Amp) by Th39;
  gcd(r,s,Amp) = 1.R by A4,Th38;
  then
A21: gcd(((r1 * s) + (s1 * r)),(d * r),Amp) = gcd(((r1 * s) + (s1 * r)),d,
  Amp) by A20,A19,Th29,Th37;
  r2 * s = (1.R * r2) * s by VECTSP_1:def 8
    .= ((d/d) * r2) * s by A4,Th9
    .= ((d * r2)/d) * s by A4,A13,Th11
    .= s * (d * r) by A14,A4,A13,Th11;
  hence thesis by A12,A21,Th37;
end;

::$N Henrici Theorem
theorem Th41:
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R
  holds gcd(r1,r2,Amp) = 1.R & gcd(s1,s2,Amp) = 1.R & r2 <> 0.R & s2 <> 0.R
implies gcd(((r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp))), ((r2/gcd(s1,r2,Amp)) *
  (s2/gcd(r1,s2,Amp))),Amp) = 1.R
proof
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: gcd(r1,r2,Amp) = 1.R and
A2: gcd(s1,s2,Amp) = 1.R and
A3: r2 <> 0.R and
A4: s2 <> 0.R;
  set d1 = gcd(r1,s2,Amp);
A5: d1 <> 0.R by A4,Th33;
  set d2 = gcd(s1,r2,Amp);
  set s19 = s1/d2;
  set r29 = r2/d2;
A6: d2 <> 0.R by A3,Th33;
  then
A7: gcd(s19,r29,Amp) = 1.R by Th38;
  set r19 = r1/d1;
A8: gcd(r19,r29,Amp) divides r29 by Def12;
  d2 divides r2 by Def12;
  then r29 * d2 = r2 by A6,Def4;
  then r29 divides r2 by Def1;
  then
A9: gcd(r19,r29,Amp) divides r2 by A8,Th2;
A10: gcd(r19,r29,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
  d1 divides r1 by Def12;
  then r19 * d1 = r1 by A5,Def4;
  then
A11: r19 divides r1 by Def1;
  1.R * gcd(r19,r29,Amp) = gcd(r19,r29,Amp) by VECTSP_1:def 8;
  then
A12: 1.R divides gcd(r19,r29,Amp) by Def1;
  gcd(r19,r29,Amp) divides r19 by Def12;
  then gcd(r19,r29,Amp) divides r1 by A11,Th2;
  then gcd(r19,r29,Amp) divides gcd(r1,r2,Amp) by A9,Def12;
  then gcd(r19,r29,Amp) is_associated_to 1.R by A1,A12,Def3;
  then gcd(r19,r29,Amp) = 1.R by A10,Th22;
  then
A13: gcd(r29,r19,Amp) = 1.R by Th29;
  set s29 = s2/d1;
A14: gcd(s19,s29,Amp) divides s29 by Def12;
  d1 divides s2 by Def12;
  then s29 * d1 = s2 by A5,Def4;
  then s29 divides s2 by Def1;
  then
A15: gcd(s19,s29,Amp) divides s2 by A14,Th2;
A16: gcd(s19,s29,Amp) is Element of Amp & 1.R is Element of Amp by Def8,Def12;
  d2 divides s1 by Def12;
  then s19 * d2 = s1 by A6,Def4;
  then
A17: s19 divides s1 by Def1;
  1.R * gcd(s19,s29,Amp) = gcd(s19,s29,Amp) by VECTSP_1:def 8;
  then
A18: 1.R divides gcd(s19,s29,Amp) by Def1;
  gcd(s19,s29,Amp) divides s19 by Def12;
  then gcd(s19,s29,Amp) divides s1 by A17,Th2;
  then gcd(s19,s29,Amp) divides gcd(s1,s2,Amp) by A15,Def12;
  then gcd(s19,s29,Amp) is_associated_to 1.R by A2,A18,Def3;
  then
A19: gcd(s19,s29,Amp) = 1.R by A16,Th22;
A20: gcd(s29,r19,Amp) = gcd((r1/d1),(s2/d1),Amp) by Th29
    .= 1.R by A5,Th38;
  gcd((r19 * s19),r29,Amp) = gcd(r29,(r19 * s19),Amp) by Th29
    .= gcd(r29,s19,Amp) by A13,Th37
    .= 1.R by A7,Th29;
  then gcd((r19 * s19),(r29 * s29),Amp) = gcd((r19 * s19),s29,Amp) by Th37
    .= gcd(s29,(r19 * s19),Amp) by Th29
    .= gcd(s29,s19,Amp) by A20,Th37
    .= 1.R by A19,Th29;
  hence thesis;
end;

begin

:: Properties of the Algorithms

definition
  let R be gcd-like associative well-unital non empty multLoopStr;
  let Amp be AmpleSet of R;
  let x,y be Element of R;
  pred x,y are_canonical_wrt Amp means
  :Def13:
  gcd(x,y,Amp) = 1.R;
end;

theorem Th42:
  for Amp,Amp9 being AmpleSet of R for x,y being Element of R st x
  ,y are_canonical_wrt Amp holds x,y are_canonical_wrt Amp9
proof
  let Amp,Amp9 be AmpleSet of R;
  let x,y be Element of R;
  1.R * x = x by VECTSP_1:def 8;
  then
A1: 1.R divides x by Def1;
  1.R * y = y by VECTSP_1:def 8;
  then
A2: 1.R divides y by Def1;
  assume x,y are_canonical_wrt Amp;
  then gcd(x,y,Amp) = 1.R by Def13;
  then
A3: for z being Element of R st z divides x & z divides y holds z divides 1.
  R by Def12;
  1.R in Amp9 by Def8;
  then gcd(x,y,Amp9) = 1.R by A3,A1,A2,Def12;
  hence thesis by Def13;
end;

definition
  let R be gcd-like associative well-unital non empty multLoopStr;
  let x,y be Element of R;
  pred x,y are_co-prime means
  :Def14:
  ex Amp being AmpleSet of R st gcd(x,y, Amp) = 1.R;
end;

definition
  let R be gcdDomain;
  let x,y be Element of R;
  redefine pred x,y are_co-prime;
  symmetry
  proof
    let x,y be Element of R;
    given Amp being AmpleSet of R such that
A1: gcd(x,y,Amp) = 1.R;
    gcd(y,x,Amp) = 1.R by A1,Th29;
    hence thesis by Def14;
  end;
end;

theorem Th43:
  for Amp being AmpleSet of R for x,y being Element of R holds x,y
  are_co-prime implies gcd(x,y,Amp) = 1.R
proof
  let Amp be AmpleSet of R;
  let x,y be Element of R;
  assume x,y are_co-prime;
  then consider Amp9 being AmpleSet of R such that
A1: gcd(x,y,Amp9) = 1.R by Def14;
  x,y are_canonical_wrt Amp9 by A1,Def13;
  then x,y are_canonical_wrt Amp by Th42;
  hence thesis by Def13;
end;

definition
  let R be gcd-like associative well-unital non empty multLoopStr_0;
  let Amp be AmpleSet of R;
  let x,y be Element of R;
  pred x,y are_normalized_wrt Amp means
  :Def15:
  gcd(x,y,Amp) = 1.R & y in Amp & y <> 0.R;
end;

:: Addition

definition
  let R be gcdDomain;
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: r1,r2 are_co-prime and
A2: s1,s2 are_co-prime and
A3: r2 = NF(r2,Amp) and
A4: s2 = NF(s2,Amp);
  func add1(r1,r2,s1,s2,Amp) -> Element of R equals
  :Def16:
  s1 if r1 = 0.R, r1
  if s1 = 0.R, (r1 * s2) + (r2 * s1) if gcd(r2,s2,Amp) = 1.R, 0.R if (r1 * (s2/
gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R otherwise ((r1 * (s2/gcd(r2
,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1
  * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp);
  coherence;
  consistency
  proof
A5: gcd(s1,s2,Amp) = 1.R by A2,Th43;
A6: s1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R
    holds z = r1 iff z = (r1 * s2) + (r2 * s1)
    proof
      assume that
A7:   s1 = 0.R and
      gcd(r2,s2,Amp) = 1.R;
A8:   s2 = 1.R by A4,A5,A7,Th30;
      let z be Element of R;
      (r1 * s2) + (r2 * s1) = (r1 * s2) + 0.R by A7,VECTSP_1:7
        .= r1 * 1.R by A8,RLVECT_1:4
        .= r1 by VECTSP_1:def 4;
      hence thesis;
    end;
A9: s1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
    0.R implies for z being Element of R holds z = r1 iff z = 0.R
    proof
A10:  1.R <> 0.R;
      assume that
A11:  s1 = 0.R and
A12:  (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
      let z be Element of R;
A13:  s2 = 1.R by A4,A5,A11,Th30;
      then
A14:  gcd(r2,s2,Amp) = 1.R by Th32;
      0.R = (r1*(s2/gcd(r2,s2,Amp)))+0.R by A11,A12,VECTSP_1:7
        .= r1*(1.R/gcd(r2,s2,Amp)) by A13,RLVECT_1:4
        .= r1*1.R by A14,A10,Th9
        .= r1 by VECTSP_1:def 4;
      hence thesis;
    end;
A15: gcd(r1,r2,Amp) = 1.R by A1,Th43;
A16: r1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R holds
    z = s1 iff z = (r1 * s2) + (r2 * s1)
    proof
      assume that
A17:  r1 = 0.R and
      gcd(r2,s2,Amp) = 1.R;
A18:  r2 = 1.R by A3,A15,A17,Th30;
      let z be Element of R;
      (r1 * s2) + (r2 * s1) = 0.R + (r2 * s1) by A17,VECTSP_1:7
        .= 1.R * s1 by A18,RLVECT_1:4
        .= s1 by VECTSP_1:def 8;
      hence thesis;
    end;
A19: r1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
    0.R implies for z being Element of R holds z = s1 iff z = 0.R
    proof
A20:  1.R <> 0.R;
      assume that
A21:  r1 = 0.R and
A22:  (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
      let z be Element of R;
A23:  r2 = 1.R by A3,A15,A21,Th30;
      then
A24:  gcd(r2,s2,Amp) = 1.R by Th32;
      0.R = 0.R+(s1*(r2/gcd(r2,s2,Amp))) by A21,A22,VECTSP_1:7
        .= s1*(1.R/gcd(r2,s2,Amp)) by A23,RLVECT_1:4
        .= s1*1.R by A24,A20,Th9
        .= s1 by VECTSP_1:def 4;
      hence thesis;
    end;
    gcd(r2,s2,Amp) = 1.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,
s2,Amp))) = 0.R implies for z being Element of R holds z = (r1 * s2) + (r2 * s1
    ) iff z = 0.R
    proof
      assume
A25:  gcd(r2,s2,Amp) = 1.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/
      gcd(r2,s2,Amp) )) = 0.R;
      let z be Element of R;
      0.R = (r1 * s2) + (s1 * (r2/1.R)) by A25,Th10
        .= (r1 * s2) + (s1 * r2) by Th10;
      hence thesis;
    end;
    hence thesis by A16,A19,A6,A9;
  end;
end;

definition
  let R be gcdDomain;
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: r1,r2 are_co-prime and
A2: s1,s2 are_co-prime and
A3: r2 = NF(r2,Amp) and
A4: s2 = NF(s2,Amp);
  func add2(r1,r2,s1,s2,Amp) -> Element of R equals
  :Def17:
  s2 if r1 = 0.R, r2
if s1 = 0.R, r2 * s2 if gcd(r2,s2,Amp) = 1.R, 1.R if (r1 * (s2/gcd(r2,s2,Amp)))
+ (s1 * (r2/gcd(r2,s2,Amp))) = 0.R otherwise (r2 * (s2/gcd(r2,s2,Amp))) / gcd((
  r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp);
  coherence;
  consistency
  proof
A5: gcd(r2,s2,Amp) = 1.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,
s2,Amp))) = 0.R implies for z being Element of R holds z = r2 * s2 iff z = 1.R
    proof
      assume that
A6:   gcd(r2,s2,Amp) = 1.R and
A7:   (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
A8:   0.R = (r1 * s2) + (s1 * (r2/1.R)) by A6,A7,Th10
        .= (r1 * s2) + (s1 * r2) by Th10;
      then
A9:   r1 * s2 = -(s1 * r2) by RLVECT_1:6;
A10:  s1 * r2 = -(r1 * s2) by A8,RLVECT_1:6;
      gcd(s2,s1,Amp) = 1.R by A2,Th43;
      then gcd(s2,s1*r2,Amp) = gcd(s2,r2,Amp) by Th37
        .= 1.R by A6,Th29;
      then 1.R = gcd(1.R*s2,-(r1*s2),Amp) by A10,VECTSP_1:def 8
        .= gcd(1.R*s2,(-r1)*s2,Amp) by VECTSP_1:8;
      then
A11:  1.R is_associated_to s2 * gcd(1.R,(-r1),Amp) by Th36;
      let z be Element of R;
A12:  1.R in Amp by Th22;
      gcd(r2,r1,Amp) = 1.R by A1,Th43;
      then gcd(r2,r1*s2,Amp) = 1.R by A6,Th37;
      then 1.R = gcd(1.R*r2,-(s1*r2),Amp) by A9,VECTSP_1:def 8
        .= gcd(1.R*r2,(-s1)*r2,Amp) by VECTSP_1:8;
      then
A13:  1.R is_associated_to r2 * gcd(1.R,(-s1),Amp) by Th36;
      s2 * gcd(1.R,(-r1),Amp) = s2 * 1.R by Th32
        .= s2 by VECTSP_1:def 4;
      then
A14:  s2 = 1.R by A4,A12,A11,Def9;
      r2 * gcd(1.R,(-s1),Amp) = r2 * 1.R by Th32
        .= r2 by VECTSP_1:def 4;
      then r2 = 1.R by A3,A13,A12,Def9;
      hence thesis by A14,VECTSP_1:def 4;
    end;
A15: gcd(r1,r2,Amp) = 1.R by A1,Th43;
A16: r1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R
    holds z = s2 iff z = r2 * s2
    proof
      assume that
A17:  r1 = 0.R and
      gcd(r2,s2,Amp) = 1.R;
      let z be Element of R;
      r2 = 1.R by A3,A15,A17,Th30;
      hence thesis by VECTSP_1:def 8;
    end;
A18: gcd(s1,s2,Amp) = 1.R by A2,Th43;
A19: s1 = 0.R & gcd(r2,s2,Amp) = 1.R implies for z being Element of R
    holds z = r2 iff z = r2 * s2
    proof
      assume that
A20:  s1 = 0.R and
      gcd(r2,s2,Amp) = 1.R;
      let z be Element of R;
      s2 = 1.R by A4,A18,A20,Th30;
      hence thesis by VECTSP_1:def 4;
    end;
A21: s1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
    0.R implies for z being Element of R holds z = r2 iff z = 1.R
    proof
A22:  1.R <> 0.R;
      assume that
A23:  s1 = 0.R and
A24:  (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
      let z be Element of R;
A25:  s2 = 1.R by A4,A18,A23,Th30;
      then
A26:  gcd(r2,s2,Amp) = 1.R by Th32;
      0.R = (r1*(s2/gcd(r2,s2,Amp)))+0.R by A23,A24,VECTSP_1:7
        .= r1*(1.R/gcd(r2,s2,Amp)) by A25,RLVECT_1:4
        .= r1*1.R by A26,A22,Th9
        .= r1 by VECTSP_1:def 4;
      hence thesis by A3,A15,Th30;
    end;
A27: r1 = 0.R & (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) =
    0.R implies for z being Element of R holds z = s2 iff z = 1.R
    proof
A28:  1.R <> 0.R;
      assume that
A29:  r1 = 0.R and
A30:  (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
      let z be Element of R;
A31:  r2 = 1.R by A3,A15,A29,Th30;
      then
A32:  gcd(r2,s2,Amp) = 1.R by Th32;
      0.R = 0.R+(s1*(r2/gcd(r2,s2,Amp))) by A29,A30,VECTSP_1:7
        .= s1*(1.R/gcd(r2,s2,Amp)) by A31,RLVECT_1:4
        .= s1*1.R by A32,A28,Th9
        .= s1 by VECTSP_1:def 4;
      hence thesis by A4,A18,Th30;
    end;
    r1 = 0.R & s1 = 0.R implies for z being Element of R holds z = s2 iff
    z = r2
    proof
      assume that
A33:  r1 = 0.R and
A34:  s1 = 0.R;
      let z be Element of R;
      r2 = 1.R by A3,A15,A33,Th30;
      hence thesis by A4,A18,A34,Th30;
    end;
    hence thesis by A16,A27,A19,A21,A5;
  end;
end;

theorem
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt
Amp implies add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp) are_normalized_wrt Amp
proof
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp;
A4: r2 <> 0.R by A2,Def15;
  r2 in Amp by A2,Def15;
  then
A5: r2 = NF(r2,Amp) by Def9;
  s2 in Amp by A3,Def15;
  then
A6: s2 = NF(s2,Amp) by Def9;
A7: gcd(r1,r2,Amp) = 1.R by A2,Def15;
  then
A8: r1,r2 are_co-prime by Def14;
A9: gcd(s1,s2,Amp) = 1.R by A3,Def15;
  then
A10: s1,s2 are_co-prime by Def14;
A11: s2 <> 0.R by A3,Def15;
  now
    per cases;
    case
A12:  r1 = 0.R;
      then add2(r1,r2,s1,s2,Amp) = s2 by A5,A6,A8,A10,Def17;
      hence thesis by A3,A5,A6,A8,A10,A12,Def16;
    end;
    case
A13:  s1 = 0.R;
      then add2(r1,r2,s1,s2,Amp) = r2 by A5,A6,A8,A10,Def17;
      hence thesis by A2,A5,A6,A8,A10,A13,Def16;
    end;
    case
A14:  gcd(r2,s2,Amp) = 1.R;
      then
A15:  add2(r1,r2,s1,s2,Amp) = r2 * s2 by A5,A6,A8,A10,Def17;
      add1(r1,r2,s1,s2,Amp) = (r1 * s2) + (r2 * s1) by A5,A6,A8,A10,A14,Def16;
      then
A16:  gcd(add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp),Amp) = gcd(((r1 * (
      s2/1.R)) + (s1 * r2)), (r2 * s2),Amp) by A15,Th10
        .= gcd((r1 * (s2/1.R)) + (s1 * (r2/1.R)), (r2 * s2),Amp) by Th10
        .= gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), (r2
      * (s2/gcd(r2,s2,Amp))),Amp) by A14,Th10
        .= gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(
      r2,s2,Amp),Amp) by A4,A7,A9,Th40
        .= 1.R by A14,Th32;
      reconsider r2,s2 as Element of Amp by A2,A3,Def15;
      r2 * s2 in Amp & r2 * s2 <> 0.R by A1,A4,A11,Def10,VECTSP_2:def 1;
      hence thesis by A15,A16,Def15;
    end;
    case
A17:  (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
A18:  1.R in Amp & 1.R <> 0.R by Th22;
A19:  add2(r1,r2,s1,s2,Amp) = 1.R by A5,A6,A8,A10,A17,Def17;
      then gcd(add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp),Amp) = 1.R by Th32;
      hence thesis by A19,A18,Def15;
    end;
    case
      r1 <> 0.R & s1 <> 0.R & gcd(r2,s2,Amp) <> 1.R & (r1 * (s2/gcd(
      r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) <> 0.R;
      then
A20:  add1(r1,r2,s1,s2,Amp) = ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd
(r2,s2,Amp )))) / gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))))
, gcd(r2,s2,Amp),Amp) & add2(r1,r2,s1,s2,Amp) = (r2 * (s2/gcd(r2,s2,Amp))) /
gcd(((r1 * ( s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))), gcd(r2,s2,Amp),
      Amp) by A5,A6,A8,A10,Def16,Def17;
      gcd(r2,s2,Amp) <> 0.R by A4,Th33;
      then
A21:  gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
      ,s2,Amp),Amp) <> 0.R by Th33;
      gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), (r2 *
(s2/gcd(r2,s2,Amp))),Amp) = gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,
      s2,Amp))), gcd(r2,s2,Amp),Amp) by A4,A7,A9,Th40;
      then
A22:  gcd( ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))) /
gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp
), ((r2 * (s2/gcd(r2,s2,Amp)))) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/
      gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp), Amp) = 1.R by A21,Th38;
      reconsider r2,s2 as Element of Amp by A2,A3,Def15;
A23:  gcd(r2,s2,Amp) divides s2 by Def12;
      reconsider z2 = gcd(((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,
      Amp)))), gcd(r2,s2,Amp),Amp) as Element of Amp by Def12;
A24:  gcd(r2,s2,Amp) <> 0.R by A4,Th33;
      then
A25:  z2 <> 0.R by Th33;
      gcd(r2,s2,Amp) in Amp by Def12;
      then reconsider z3 = s2/gcd(r2,s2,Amp) as Element of Amp by A1,A23,A24
,Th27;
      r2 * z3 in Amp by A1,Def10;
      then reconsider z1 = r2 * (s2/gcd(r2,s2,Amp)) as Element of Amp;
A26:  r2 * s2 <> 0.R by A4,A11,VECTSP_2:def 1;
A27:  gcd(r2,s2,Amp) divides r2 * s2 by A23,Th7;
      then z1 = (r2 * s2)/gcd(r2,s2,Amp) by A23,A24,Th11;
      then
A28:  z1 <> 0.R by A24,A26,A27,Th8;
      z2 divides gcd(r2,s2,Amp) & gcd(r2,s2,Amp) divides r2 by Def12;
      then
A29:  z2 divides r2 by Th2;
      then z2 divides z1 by Th7;
      then
A30:  z1 / z2 <> 0.R by A25,A28,Th8;
      z1 / z2 in Amp by A1,A29,A25,Th7,Th27;
      hence thesis by A20,A22,A30,Def15;
    end;
  end;
  hence thesis;
end;

theorem
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies add1(r1,r2,
  s1,s2,Amp) * (r2 * s2) = add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
proof
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp;
  gcd(r1,r2,Amp) = 1.R by A1,Def15;
  then
A3: r1,r2 are_co-prime by Def14;
  s2 in Amp by A2,Def15;
  then
A4: s2 = NF(s2,Amp) by Def9;
  gcd(s1,s2,Amp) = 1.R by A2,Def15;
  then
A5: s1,s2 are_co-prime by Def14;
  r2 in Amp by A1,Def15;
  then
A6: r2 = NF(r2,Amp) by Def9;
A7: r2 <> 0.R by A1,Def15;
  now
    per cases;
    case
A8:   r1 = 0.R;
      then
A9:   add1(r1,r2,s1,s2,Amp) = s1 by A3,A5,A6,A4,Def16;
      add2(r1,r2,s1,s2,Amp) = s2 by A3,A5,A6,A4,A8,Def17;
      then
      add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) = s2 * (0.R + (s1 *
      r2)) by A8,VECTSP_1:7
        .= s2 * (s1 * r2) by RLVECT_1:4
        .= add1(r1,r2,s1,s2,Amp) * (r2 * s2) by A9,GROUP_1:def 3;
      hence thesis;
    end;
    case
A10:  s1 = 0.R;
      then
A11:  add1(r1,r2,s1,s2,Amp) = r1 by A3,A5,A6,A4,Def16;
      add2(r1,r2,s1,s2,Amp) = r2 by A3,A5,A6,A4,A10,Def17;
      then
      add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) = r2 * ((r1 * s2) +
      0.R) by A10,VECTSP_1:7
        .= r2 * (r1 * s2) by RLVECT_1:4
        .= add1(r1,r2,s1,s2,Amp) * (r2 * s2) by A11,GROUP_1:def 3;
      hence thesis;
    end;
    case
A12:  gcd(r2,s2,Amp) = 1.R;
      then add2(r1,r2,s1,s2,Amp) = r2 * s2 by A3,A5,A6,A4,Def17;
      hence thesis by A3,A5,A6,A4,A12,Def16;
    end;
    case
A13:  (r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) = 0.R;
A14:  (r1 * s2) + (s1 * r2) = 0.R
      proof
A15:    gcd(r2,s2,Amp) divides r2 by Def12;
        then
A16:    gcd(r2,s2,Amp) divides s1 * r2 by Th7;
A17:    gcd(r2,s2,Amp) divides s2 by Def12;
        then consider f being Element of R such that
A18:    gcd(r2,s2,Amp) * f = s2 by Def1;
A19:    gcd(r2,s2,Amp) <> 0.R by A7,Th33;
        consider e being Element of R such that
A20:    gcd(r2,s2,Amp) * e = r2 by A15,Def1;
        gcd(r2,s2,Amp) * ((e * s1)+(f * r1)) = (gcd(r2,s2,Amp) * (e * s1)
        )+(gcd(r2,s2,Amp) * (f * r1)) by VECTSP_1:def 2
          .= ((gcd(r2,s2,Amp) * e) * s1)+(gcd(r2,s2,Amp) * (f * r1)) by
GROUP_1:def 3
          .= (r1 * s2)+(s1 * r2) by A20,A18,GROUP_1:def 3;
        then
A21:    gcd(r2,s2,Amp) divides (r1 * s2) + (s1 * r2) by Def1;
A22:    gcd(r2,s2,Amp) divides r1 * s2 by A17,Th7;
        then 0.R = (r1 * s2)/gcd(r2,s2,Amp) + (s1 * (r2/gcd(r2,s2,Amp))) by A13
,A19,A17,Th11
          .= (r1 * s2)/gcd(r2,s2,Amp) + (s1 * r2)/gcd(r2,s2,Amp) by A19,A15,A16
,Th11;
        then
A23:    0.R = ((r1 * s2) + (s1 * r2)) / gcd(r2,s2,Amp) by A19,A22,A16,A21,Th12;
        0.R = 0.R * gcd(r2,s2,Amp) by VECTSP_1:7
          .= ((r1 * s2) + (s1 * r2)) by A19,A21,A23,Def4;
        hence thesis;
      end;
      add1(r1,r2,s1,s2,Amp) = 0.R by A3,A5,A6,A4,A13,Def16;
      then add1(r1,r2,s1,s2,Amp) * (r2 * s2) = 0.R by VECTSP_1:7
        .= add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A14,VECTSP_1:7;
      hence thesis;
    end;
    case
A24:  r1 <> 0.R & s1 <> 0.R & gcd(r2,s2,Amp) <> 1.R & (r1 * (s2/gcd(
      r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))) <> 0.R;
A25:  gcd(r2,s2,Amp) divides s2 by Def12;
      then
A26:  gcd(r2,s2,Amp) divides r1 * s2 by Th7;
      then
A27:  gcd(r2,s2,Amp) divides ((r1 * s2) * r2) by Th7;
      then
A28:  gcd(r2,s2,Amp) divides (((r1 * s2) * r2) * s2) by Th7;
A29:  add1(r1,r2,s1,s2,Amp) = ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd
(r2,s2,Amp)))) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))),
      gcd(r2,s2,Amp),Amp) by A3,A5,A6,A4,A24,Def16;
A30:  gcd(r2,s2,Amp) divides r2 by Def12;
      then
A31:  gcd(r2,s2,Amp) divides s1 * r2 by Th7;
      gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
      ,s2,Amp),Amp) divides gcd(r2,s2,Amp) by Def12;
      then
      gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
      ,s2,Amp),Amp) divides r2 by A30,Th2;
      then
A32:  gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
      ,s2,Amp),Amp) divides (r2 * (s2/gcd(r2,s2,Amp))) by Th7;
      then
A33:  gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides (r2 * (s2/gcd(r2,s2,Amp))) * ((r1 * s2)+(s1 * r2)) by Th7
;
A34:  gcd(r2,s2,Amp) divides ((s1 * r2) * r2) by A30,Th7;
      then
A35:  gcd(r2,s2,Amp) divides (((s1 * r2) * r2) * s2) by Th7;
A36:  gcd(r2,s2,Amp) divides (r2 * s2) by A30,Th7;
      then
A37:  gcd(r2,s2,Amp) divides ((r2 * s2) * r1) by Th7;
      then
A38:  gcd(r2,s2,Amp) divides (((r2 * s2) * r1) * s2) by Th7;
A39:  gcd(r2,s2,Amp) divides ((r2 * s2) * s1) by A36,Th7;
      then
A40:  gcd(r2,s2,Amp) divides (((r2 * s2) * s1) * r2) by Th7;
A41:  add2(r1,r2,s1,s2,Amp) = (r2 * (s2/gcd(r2,s2,Amp))) / gcd((r1 * (s2/
gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp) by A3,A5,A6
,A4,A24,Def17;
A42:  gcd(r2,s2,Amp) <> 0.R by A7,Th33;
      then
A43:  gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
      ,s2,Amp),Amp) <> 0.R by Th33;
A44:  (r2 * (s2/gcd(r2,s2,Amp))) * ((r1 * s2) + (s1 * r2)) = ((r2 * (s2/
gcd(r2,s2,Amp))) * (r1 * s2)) + ((r2 * (s2/gcd(r2,s2,Amp))) * (s1 * r2)) by
VECTSP_1:def 2
        .= (((r2 * (s2/gcd(r2,s2,Amp))) * r1) * s2) + ((r2 * (s2/gcd(r2,s2,
      Amp))) * (s1 * r2)) by GROUP_1:def 3
        .= (((r2 * (s2/gcd(r2,s2,Amp))) * r1) * s2) + (((r2 * (s2/gcd(r2,s2,
      Amp))) * s1) * r2) by GROUP_1:def 3
        .= ((((r2 * s2)/gcd(r2,s2,Amp)) * r1) * s2) + (((r2 * (s2/gcd(r2,s2,
      Amp))) * s1) * r2) by A42,A25,A36,Th11
        .= ((((r2 * s2)/gcd(r2,s2,Amp)) * r1) * s2) + ((((r2 * s2)/gcd(r2,s2
      ,Amp)) * s1) * r2) by A42,A25,A36,Th11
        .= ((((r2 * s2) * r1)/gcd(r2,s2,Amp)) * s2) + ((((r2 * s2)/gcd(r2,s2
      ,Amp)) * s1) * r2) by A42,A36,A37,Th11
        .= ((((r2 * s2) * r1)/gcd(r2,s2,Amp)) * s2) + ((((r2 * s2) * s1)/gcd
      (r2,s2,Amp)) * r2) by A42,A36,A39,Th11
        .= ((((r2 * s2) * r1) * s2)/gcd(r2,s2,Amp)) + ((((r2 * s2) * s1)/gcd
      (r2,s2,Amp)) * r2) by A42,A37,A38,Th11
        .= (((r1 * (s2 * r2)) * s2)/gcd(r2,s2,Amp)) + ((((r2 * s2) * s1) *
      r2)/gcd(r2,s2,Amp)) by A42,A39,A40,Th11
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((r2 * s2) * s1) *
      r2)/gcd(r2,s2,Amp)) by GROUP_1:def 3
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((s1 * ((r2 * s2) * r2
      ))/gcd(r2,s2,Amp)) by GROUP_1:def 3
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((s1 * ((r2 * r2) * s2
      ))/gcd(r2,s2,Amp)) by GROUP_1:def 3
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + (((s1 * (r2 * r2)) *
      s2)/gcd(r2,s2,Amp)) by GROUP_1:def 3
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((s1 * r2) * r2) *
      s2)/gcd(r2,s2,Amp)) by GROUP_1:def 3;
A45:  ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp)))) * (r2 *
s2) = ((r1 * (s2/gcd(r2,s2,Amp))) * (r2 * s2)) + ((s1 * (r2/gcd(r2,s2,Amp))) *
      (r2 * s2)) by VECTSP_1:def 7
        .= (((r1 * s2)/gcd(r2,s2,Amp)) * (r2 * s2)) + ((s1 * (r2/gcd(r2,s2,
      Amp))) * (r2 * s2)) by A42,A25,A26,Th11
        .= (((r1 * s2)/gcd(r2,s2,Amp)) * (r2 * s2)) + (((s1 * r2)/gcd(r2,s2,
      Amp)) * (r2 * s2)) by A42,A30,A31,Th11
        .= ((((r1 * s2)/gcd(r2,s2,Amp)) * r2) * s2) + (((s1 * r2)/gcd(r2,s2,
      Amp)) * (r2 * s2)) by GROUP_1:def 3
        .= ((((r1 * s2)/gcd(r2,s2,Amp)) * r2) * s2) + ((((s1 * r2)/gcd(r2,s2
      ,Amp)) * r2) * s2) by GROUP_1:def 3
        .= ((((r1 * s2) * r2)/gcd(r2,s2,Amp)) * s2) + ((((s1 * r2)/gcd(r2,s2
      ,Amp)) * r2) * s2) by A42,A26,A27,Th11
        .= ((((r1 * s2) * r2)/gcd(r2,s2,Amp)) * s2) + ((((s1 * r2) * r2)/gcd
      (r2,s2,Amp)) * s2) by A42,A31,A34,Th11
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((s1 * r2) * r2)/gcd
      (r2,s2,Amp)) * s2) by A42,A27,A28,Th11
        .= ((((r1 * s2) * r2) * s2)/gcd(r2,s2,Amp)) + ((((s1 * r2) * r2) *
      s2)/gcd(r2,s2,Amp)) by A42,A34,A35,Th11;
A46:  gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides ((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))))
      by Def12;
      then
      gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1 * (r2/gcd(r2,s2,Amp))), gcd(r2
,s2,Amp),Amp) divides ((r1*(s2/gcd(r2,s2,Amp)))+(s1 * (r2/gcd(r2,s2,Amp)))) * (
      r2*s2) by Th7;
      then add1(r1,r2,s1,s2,Amp) * (r2 * s2) = (((r1 * (s2/gcd(r2,s2,Amp)))+(
s1 * (r2/gcd(r2,s2,Amp)))) * (r2 * s2)) / gcd((r1 * (s2/gcd(r2,s2,Amp))) + (s1
      * (r2/gcd(r2,s2,Amp))), gcd(r2,s2,Amp),Amp) by A29,A43,A46,Th11
        .= add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2)) by A41,A45,A44,A43
,A32,A33,Th11;
      hence thesis;
    end;
  end;
  hence thesis;
end;

:: Multiplication

definition
  let R be gcdDomain;
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  func mult1(r1,r2,s1,s2,Amp) -> Element of R equals
  :Def18:
  0.R if r1 = 0.R
or s1 = 0.R, r1 * s1 if r2 = 1.R & s2 = 1.R, (r1 * s1)/gcd(r1,s2,Amp) if s2 <>
0.R & r2 = 1.R, (r1 * s1)/gcd(s1,r2,Amp) if r2 <> 0.R & s2 = 1.R otherwise (r1/
  gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp));
  coherence;
  consistency
  proof
A1: (r1 = 0.R or s1 = 0.R) & r2 <> 0.R & s2 = 1.R implies for z being
    Element of R holds z = 0.R iff z = (r1 * s1)/gcd(s1,r2,Amp)
    proof
      set d = (r1 * s1)/gcd(s1,r2,Amp);
      assume that
A2:   r1 = 0.R or s1 = 0.R and
A3:   r2 <> 0.R and
      s2 = 1.R;
A4:   gcd(s1,r2,Amp) <> 0.R by A3,Th33;
      let z be Element of R;
A5:   r1 * s1 = 0.R
      proof
        now
          per cases by A2;
          case
            r1 = 0.R;
            hence thesis by VECTSP_1:7;
          end;
          case
            s1 = 0.R;
            hence thesis by VECTSP_1:7;
          end;
        end;
        hence thesis;
      end;
      gcd(s1,r2,Amp) divides s1 by Def12;
      then gcd(s1,r2,Amp) divides r1 * s1 by Th7;
      then d * gcd(s1,r2,Amp) = 0.R by A5,A4,Def4;
      hence thesis by A4,VECTSP_2:def 1;
    end;
A6: (r1 = 0.R or s1 = 0.R) & s2 <> 0.R & r2 = 1.R implies for z being
    Element of R holds z = 0.R iff z = (r1 * s1)/gcd(r1,s2,Amp)
    proof
      set d = (r1 * s1)/gcd(r1,s2,Amp);
      assume that
A7:  r1 = 0.R or s1 = 0.R and
A8:  s2 <> 0.R and
      r2 = 1.R;
A9:  gcd(r1,s2,Amp) <> 0.R by A8,Th33;
      let z be Element of R;
A10:  r1 * s1 = 0.R
      proof
        now
          per cases by A7;
          case
            r1 = 0.R;
            hence thesis by VECTSP_1:7;
          end;
          case
            s1 = 0.R;
            hence thesis by VECTSP_1:7;
          end;
        end;
        hence thesis;
      end;
      gcd(r1,s2,Amp) divides r1 by Def12;
      then gcd(r1,s2,Amp) divides r1 * s1 by Th7;
      then d * gcd(r1,s2,Amp) = 0.R by A10,A9,Def4;
      hence thesis by A9,VECTSP_2:def 1;
    end;
A11: r2 = 1.R & s2 = 1.R & r2 <> 0.R & s2 = 1.R implies for z being
    Element of R holds z = r1 * s1 iff z = (r1 * s1)/gcd(s1,r2,Amp)
    proof
      assume that
A12:  r2 = 1.R and
      s2 = 1.R and
      r2 <> 0.R and
      s2 = 1.R;
      gcd(s1,r2,Amp) = 1.R by A12,Th32;
      hence thesis by Th10;
    end;
    r2 = 1.R & s2 = 1.R & s2 <> 0.R & r2 = 1.R implies for z being
    Element of R holds z = r1 * s1 iff z = (r1 * s1)/gcd(r1,s2,Amp)
    proof
      assume that
      r2 = 1.R and
A13:  s2 = 1.R and
      s2 <> 0.R and
      r2 = 1.R;
      gcd(r1,s2,Amp) = 1.R by A13,Th32;
      hence thesis by Th10;
    end;
    hence thesis by A6,A1,A11;
  end;
end;

definition
  let R be gcdDomain;
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: r1,r2 are_co-prime and
A2: s1,s2 are_co-prime and
A3: r2 = NF(r2,Amp) and
A4: s2 = NF(s2,Amp);
  func mult2(r1,r2,s1,s2,Amp) -> Element of R equals
  :Def19:
  1.R if r1 = 0.R
or s1 = 0.R, 1.R if r2 = 1.R & s2 = 1.R, s2/gcd(r1,s2,Amp) if s2 <> 0.R & r2 =
1.R, r2/gcd(s1,r2,Amp) if r2 <> 0.R & s2 = 1.R otherwise (r2/gcd(s1,r2,Amp)) *
  (s2/gcd(r1,s2,Amp));
  coherence;
  consistency
  proof
A5: gcd(s1,s2,Amp) = 1.R by A2,Th43;
A6: (r1 = 0.R or s1 = 0.R) & s2 <> 0.R & r2 = 1.R implies for z being
    Element of R holds z = 1.R iff z = s2/gcd(r1,s2,Amp)
    proof
      assume that
A7:   r1 = 0.R or s1 = 0.R and
A8:   s2 <> 0.R and
      r2 = 1.R;
      now
        per cases by A7;
        case
          r1 = 0.R;
          then gcd(r1,s2,Amp) = s2 by A4,Th30;
          hence thesis by A8,Th9;
        end;
        case
A9:       s1 = 0.R;
A10:      1.R <> 0.R;
A11:      1.R = s2 by A4,A5,A9,Th30;
          then gcd(r1,s2,Amp) = 1.R by Th32;
          hence thesis by A11,A10,Th9;
        end;
      end;
      hence thesis;
    end;
A12: gcd(r1,r2,Amp) = 1.R by A1,Th43;
A13: (r1 = 0.R or s1 = 0.R) & r2 <> 0.R & s2 = 1.R implies for z being
    Element of R holds z = 1.R iff z = r2/gcd(s1,r2,Amp)
    proof
      assume that
A14:  r1 = 0.R or s1 = 0.R and
A15:  r2 <> 0.R and
      s2 = 1.R;
      now
        per cases by A14;
        case
          s1 = 0.R;
          then gcd(s1,r2,Amp) = r2 by A3,Th30;
          hence thesis by A15,Th9;
        end;
        case
A16:      r1 = 0.R;
A17:      1.R <> 0.R;
A18:      1.R = r2 by A3,A12,A16,Th30;
          then gcd(s1,r2,Amp) = 1.R by Th32;
          hence thesis by A18,A17,Th9;
        end;
      end;
      hence thesis;
    end;
A19: r2 = 1.R & s2 = 1.R & r2 <> 0.R & s2 = 1.R implies for z being
    Element of R holds z = 1.R iff z = r2/gcd(s1,r2,Amp)
    proof
      assume that
A20:  r2 = 1.R and
      s2 = 1.R and
A21:  r2 <> 0.R and
      s2 = 1.R;
      gcd(s1,r2,Amp) = 1.R by A20,Th32;
      hence thesis by A20,A21,Th9;
    end;
    r2 = 1.R & s2 = 1.R & s2 <> 0.R & r2 = 1.R implies for z being
    Element of R holds z = 1.R iff z = s2/gcd(r1,s2,Amp)
    proof
      assume that
      r2 = 1.R and
A22:  s2 = 1.R and
A23:  s2 <> 0.R and
      r2 = 1.R;
      gcd(r1,s2,Amp) = 1.R by A22,Th32;
      hence thesis by A22,A23,Th9;
    end;
    hence thesis by A6,A13,A19;
  end;
end;

theorem
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt
  Amp implies mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp) are_normalized_wrt
  Amp
proof
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp;
A4: gcd(r1,r2,Amp) = 1.R by A2,Def15;
  then
A5: r1,r2 are_co-prime by Def14;
  s2 in Amp by A3,Def15;
  then
A6: s2 = NF(s2,Amp) by Def9;
  r2 in Amp by A2,Def15;
  then
A7: r2 = NF(r2,Amp) by Def9;
A8: r2 <> 0.R by A2,Def15;
  then
A9: gcd(s1,r2,Amp) <> 0.R by Th33;
A10: gcd(s1,s2,Amp) = 1.R by A3,Def15;
  then
A11: s1,s2 are_co-prime by Def14;
A12: s2 <> 0.R by A3,Def15;
  then
A13: gcd(r1,s2,Amp) <> 0.R by Th33;
  now
    per cases;
    case
A14:  r1 = 0.R or s1 = 0.R;
A15:  1.R in Amp & 1.R <> 0.R by Th22;
A16:  mult2(r1,r2,s1,s2,Amp) = 1.R by A5,A11,A7,A6,A14,Def19;
      then
      gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by Th32;
      hence thesis by A16,A15,Def15;
    end;
    case
A17:  r2 = 1.R & s2 = 1.R;
A18:  1.R in Amp & 1.R <> 0.R by Th22;
A19:  mult2(r1,r2,s1,s2,Amp) = 1.R by A5,A11,A7,A17,Def19;
      then
      gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by Th32;
      hence thesis by A19,A18,Def15;
    end;
    case
A20:  s2 <> 0.R & r2 = 1.R;
      then
A21:  gcd(s1,r2,Amp) = 1.R by Th32;
      then r2/gcd(s1,r2,Amp) = 1.R by A20,Th9;
      then
A22:  s2/gcd(r1,s2,Amp) = (s2/gcd(r1,s2,Amp)) * (r2/gcd(s1,r2,Amp)) by
VECTSP_1:def 4;
A23:  gcd(r1,s2,Amp) divides r1 by Def12;
      then gcd(r1,s2,Amp) divides (r1 * s1) by Th7;
      then
A24:  (r1 * s1)/gcd(r1,s2,Amp) = (r1/gcd(r1,s2,Amp)) * s1 by A13,A23,Th11
        .= (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp)) by A21,Th10;
A25:  mult2(r1,r2,s1,s2,Amp) = s2/gcd(r1,s2,Amp) by A5,A11,A7,A6,A20,Def19;
      reconsider zz = gcd(r1,s2,Amp) as Element of Amp by Def12;
A26:  gcd(r1,s2,Amp) divides s2 & gcd(r1,s2,Amp) <> 0.R by A12,Def12,Th33;
      then
A27:  s2/gcd(r1,s2,Amp) <> 0.R by A12,Th8;
      mult1(r1,r2,s1,s2,Amp) = (r1 * s1)/gcd(r1,s2,Amp) by A20,Def18;
      then
A28:  gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by A4,A10,A8
,A12,A25,A24,A22,Th41;
      reconsider s2 as Element of Amp by A3,Def15;
      s2/zz in Amp by A1,A26,Th27;
      hence thesis by A25,A28,A27,Def15;
    end;
    case
A29:  r2 <> 0.R & s2 = 1.R;
      then
A30:  gcd(r1,s2,Amp) = 1.R by Th32;
      then s2/gcd(r1,s2,Amp) = 1.R by A29,Th9;
      then
A31:  r2/gcd(s1,r2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp)) by
VECTSP_1:def 4;
A32:  gcd(s1,r2,Amp) divides s1 by Def12;
      then gcd(s1,r2,Amp) divides (r1 * s1) by Th7;
      then
A33:  (r1 * s1)/gcd(s1,r2,Amp) = r1 * (s1/gcd(s1,r2,Amp)) by A9,A32,Th11
        .= (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp)) by A30,Th10;
A34:  mult2(r1,r2,s1,s2,Amp) = r2/gcd(s1,r2,Amp) by A5,A11,A7,A6,A29,Def19;
      reconsider zz = gcd(s1,r2,Amp) as Element of Amp by Def12;
A35:  gcd(s1,r2,Amp) divides r2 & gcd(s1,r2,Amp) <> 0.R by A8,Def12,Th33;
      then
A36:  r2/gcd(s1,r2,Amp) <> 0.R by A8,Th8;
      mult1(r1,r2,s1,s2,Amp) = (r1 * s1)/gcd(s1,r2,Amp) by A29,Def18;
      then
A37:  gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by A4,A10,A8
,A12,A34,A33,A31,Th41;
      reconsider r2 as Element of Amp by A2,Def15;
      r2/zz in Amp by A1,A35,Th27;
      hence thesis by A34,A37,A36,Def15;
    end;
    case
A38:  not(r1 = 0.R or s1 = 0.R) & not(r2 = 1.R & s2 = 1.R) & not(s2
      <> 0.R & r2 = 1.R) & not(r2 <> 0.R & s2 = 1.R);
      reconsider z2 = gcd(s1,r2,Amp) as Element of Amp by Def12;
      reconsider z1 = gcd(r1,s2,Amp) as Element of Amp by Def12;
A39:  gcd(r1,s2,Amp) divides s2 & gcd(r1,s2,Amp) <> 0.R by A12,Def12,Th33;
      then
A40:  s2/gcd(r1,s2,Amp) <> 0.R by A12,Th8;
A41:  mult2(r1,r2,s1,s2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))
      by A5,A11,A7,A6,A38,Def19;
      mult1(r1,r2,s1,s2,Amp) = (r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2, Amp))
      by A38,Def18;
      then
A42:  gcd(mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp),Amp) = 1.R by A4,A10,A8
,A12,A41,Th41;
A43:  gcd(s1,r2,Amp) divides r2 & gcd(s1,r2,Amp) <> 0.R by A8,Def12,Th33;
      then
A44:  r2/gcd(s1,r2,Amp) <> 0.R by A8,Th8;
      reconsider s2 as Element of Amp by A3,Def15;
      reconsider u = s2/z1 as Element of Amp by A1,A39,Th27;
      reconsider r2 as Element of Amp by A2,Def15;
      reconsider v = r2/z2 as Element of Amp by A1,A43,Th27;
A45:  v * u <> 0.R by A40,A44,VECTSP_2:def 1;
      v * u in Amp by A1,Def10;
      hence thesis by A41,A42,A45,Def15;
    end;
  end;
  hence thesis;
end;

theorem
  for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies mult1(r1,r2
  ,s1,s2,Amp) * (r2 * s2) = mult2(r1,r2,s1,s2,Amp) * (r1 * s1)
proof
  let Amp be AmpleSet of R;
  let r1,r2,s1,s2 be Element of R;
  assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp;
  gcd(r1,r2,Amp) = 1.R by A1,Def15;
  then
A3: r1,r2 are_co-prime by Def14;
  s2 <> 0.R by A2,Def15;
  then
A4: gcd(r1,s2,Amp) <> 0.R by Th33;
  r2 in Amp by A1,Def15;
  then
A5: r2 = NF(r2,Amp) by Def9;
  gcd(s1,s2,Amp) = 1.R by A2,Def15;
  then
A6: s1,s2 are_co-prime by Def14;
  r2 <> 0.R by A1,Def15;
  then
A7: gcd(s1,r2,Amp) <> 0.R by Th33;
  s2 in Amp by A2,Def15;
  then
A8: s2 = NF(s2,Amp) by Def9;
  now
    per cases;
    case
A9:   r1 = 0.R or s1 = 0.R;
      then
A10:  mult1(r1,r2,s1,s2,Amp) = 0.R by Def18;
      now
        per cases by A9;
        case
          r1 = 0.R;
          then mult2(r1,r2,s1,s2,Amp) * (r1 * s1) = mult2(r1,r2,s1,s2,Amp) *
          0.R by VECTSP_1:7
            .= 0.R by VECTSP_1:7;
          hence thesis by A10,VECTSP_1:7;
        end;
        case
          s1 = 0.R;
          then mult2(r1,r2,s1,s2,Amp) * (r1 * s1) = mult2(r1,r2,s1,s2,Amp) *
          0.R by VECTSP_1:7
            .= 0.R by VECTSP_1:7;
          hence thesis by A10,VECTSP_1:7;
        end;
      end;
      hence thesis;
    end;
    case
A11:  r2 = 1.R & s2 = 1.R;
      then mult1(r1,r2,s1,s2,Amp) = r1 * s1 & mult2(r1,r2,s1,s2,Amp) = 1.R by
A3,A6,A5,Def18,Def19;
      hence thesis by A11,VECTSP_1:def 4;
    end;
    case
A12:  s2 <> 0.R & r2 = 1.R;
      gcd(r1,s2,Amp) divides r1 by Def12;
      then
A13:  gcd(r1,s2,Amp) divides (r1 * s1) by Th7;
      then
A14:  gcd(r1,s2,Amp) divides (r1 * s1) * s2 by Th7;
A15:  ((r1 * s1)/gcd(r1,s2,Amp)) * (r2 * s2) = ((r1 * s1)/gcd(r1,s2,Amp))
      * s2 by A12,VECTSP_1:def 8
        .= ((r1 * s1) * s2)/gcd(r1,s2,Amp) by A4,A13,A14,Th11;
A16:  mult2(r1,r2,s1,s2,Amp) = s2/gcd(r1,s2,Amp) by A3,A6,A5,A8,A12,Def19;
A17:  gcd(r1,s2,Amp) divides s2 by Def12;
      then
A18:  gcd(r1,s2,Amp) divides s2 * r1 by Th7;
      then
A19:  gcd(r1,s2,Amp) divides (s2 * r1) * s1 by Th7;
      (s2/gcd(r1,s2,Amp)) * (r1 * s1) = ((s2/gcd(r1,s2,Amp)) * r1) * s1
      by GROUP_1:def 3
        .= ((s2 * r1)/gcd(r1,s2,Amp)) * s1 by A4,A17,A18,Th11
        .= ((s2 * r1) * s1)/gcd(r1,s2,Amp) by A4,A18,A19,Th11
        .= ((r1 * s1) * s2)/gcd(r1,s2,Amp) by GROUP_1:def 3;
      hence thesis by A12,A16,A15,Def18;
    end;
    case
A20:  r2 <> 0.R & s2 = 1.R;
      gcd(s1,r2,Amp) divides s1 by Def12;
      then
A21:  gcd(s1,r2,Amp) divides (s1 * r1) by Th7;
      then
A22:  gcd(s1,r2,Amp) divides (s1 * r1) * r2 by Th7;
A23:  ((r1 * s1)/gcd(s1,r2,Amp)) * (r2 * s2) = ((r1 * s1)/gcd(s1,r2,Amp))
      * r2 by A20,VECTSP_1:def 4
        .= ((r1 * s1) * r2)/gcd(s1,r2,Amp) by A7,A21,A22,Th11;
A24:  mult2(r1,r2,s1,s2,Amp) = r2/gcd(s1,r2,Amp) by A3,A6,A5,A8,A20,Def19;
A25:  gcd(s1,r2,Amp) divides r2 by Def12;
      then
A26:  gcd(s1,r2,Amp) divides r2 * r1 by Th7;
      then
A27:  gcd(s1,r2,Amp) divides (r2 * r1) * s1 by Th7;
      (r2/gcd(s1,r2,Amp)) * (r1 * s1) = ((r2/gcd(s1,r2,Amp)) * r1) * s1
      by GROUP_1:def 3
        .= ((r2 * r1)/gcd(s1,r2,Amp)) * s1 by A7,A25,A26,Th11
        .= ((r2 * r1) * s1)/gcd(s1,r2,Amp) by A7,A26,A27,Th11
        .= ((r1 * s1) * r2)/gcd(s1,r2,Amp) by GROUP_1:def 3;
      hence thesis by A20,A24,A23,Def18;
    end;
    case
A28:  not(r1 = 0.R or s1 = 0.R) & not(r2 = 1.R & s2 = 1.R) & not(s2
      <> 0.R & r2 = 1.R) & not(r2 <> 0.R & s2 = 1.R);
A29:  gcd(s1,r2,Amp) divides r2 & gcd(r1,s2,Amp) divides s2 by Def12;
      then
A30:  (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides r2 * s2 by Th3;
      then
A31:  (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides (r2 * s2) * r1 by Th7;
      then
A32:  (gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) divides ((r2 * s2) * r1) * s1 by Th7;
A33:  gcd(r1,s2,Amp) divides r1 & gcd(s1,r2,Amp) divides s1 by Def12;
      then
A34:  (gcd(r1,s2,Amp) *gcd(s1,r2,Amp)) divides r1 * s1 by Th3;
      then
A35:  (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) divides (r1 * s1) * r2 by Th7;
      then
A36:  (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) divides ((r1 * s1) * r2) * s2 by Th7;
A37:  mult2(r1,r2,s1,s2,Amp) = (r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))
      by A3,A6,A5,A8,A28,Def19;
A38:  (gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) <> 0.R by A4,A7,VECTSP_2:def 1;
A39:  ((r2/gcd(s1,r2,Amp)) * (s2/gcd(r1,s2,Amp))) * (r1 * s1) = ((r2 * s2
      )/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * (r1 * s1) by A4,A7,A29,Th14
        .= (((r2 * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * r1) * s1 by
GROUP_1:def 3
        .= (((r2 * s2) * r1)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp))) * s1 by A38,A30
,A31,Th11
        .= (((r2 * s2) * r1) * s1)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by A38,A31
,A32,Th11
        .= (r1 * ((r2 * s2) * s1))/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3
        .= (r1 * ((s1 * r2) * s2))/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3
        .= ((r1 * (s1 * r2)) * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3
        .= (((r1 * s1) * r2) * s2)/(gcd(s1,r2,Amp) * gcd(r1,s2,Amp)) by
GROUP_1:def 3;
      ((r1/gcd(r1,s2,Amp)) * (s1/gcd(s1,r2,Amp))) * (r2 * s2) = ((r1 * s1
      )/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * (r2 * s2) by A4,A7,A33,Th14
        .= (((r1 * s1)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * r2) * s2 by
GROUP_1:def 3
        .= (((r1 * s1) * r2)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp))) * s2 by A34,A35
,A38,Th11
        .= (((r1 * s1) * r2) * s2)/(gcd(r1,s2,Amp) * gcd(s1,r2,Amp)) by A35,A36
,A38,Th11;
      hence thesis by A28,A37,A39,Def18;
    end;
  end;
  hence thesis;
end;

theorem
  for F be add-associative right_zeroed right_complementable Abelian
distributive non empty doubleLoopStr, x,y being Element of F holds (-x)*y = -
  x*y & x*(-y) = -x*y by VECTSP_1:8,9;

theorem
  for F being almost_left_invertible commutative Ring for a, b being
  Element of F st a <> 0.F & b <> 0.F holds a"*b" = (b*a)"
proof
  let F be almost_left_invertible commutative Ring;
  let a,b be Element of F such that
A1: a <> 0.F and
A2: b <> 0.F;
A3: b*a * (a"*b") = b*a*a"*b" by GROUP_1:def 3
    .= b*(a*a")*b" by GROUP_1:def 3
    .= b*1_F*b" by A1,VECTSP_1:def 10
    .= b*b" by VECTSP_1:def 4
    .= 1_F by A2,VECTSP_1:def 10;
  b*a <> 0.F by A1,A2,VECTSP_1:12;
  hence thesis by A3,VECTSP_1:def 10;
end;