:: Binary Operations on Numbers
::  by Library Committee
::
:: Received June 21, 2004
:: Copyright (c) 2004-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 XBOOLE_0, SUBSET_1, FUNCT_1, BINOP_1, XCMPLX_0, ORDINAL1,
      NUMBERS, XREAL_0, RAT_1, INT_1, ZFMISC_1, ARYTM_1, RELAT_1, ARYTM_3,
      CARD_1, SETWISEO, BINOP_2, NAT_1;
 notations XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, BINOP_1, SETWISEO,
      ORDINAL1, XCMPLX_0, XREAL_0, INT_1, NUMBERS, RAT_1;
 constructors BINOP_1, SETWISEO, XCMPLX_0, RAT_1, RELSET_1;
 registrations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, INT_1,
      RAT_1, RELSET_1;
 requirements BOOLE, SUBSET, ARITHM, NUMERALS;
 definitions BINOP_1;
 theorems BINOP_1, FUNCT_2, XCMPLX_0, XREAL_0, INT_1, RAT_1, SETWISEO, NUMBERS,
      ORDINAL1;
 schemes BINOP_1, FUNCT_2;

begin

scheme
  FuncDefUniq{C, D()->non empty set, F(Element of C())->set}: for f1,f2 being
Function of C(),D() st (for x being Element of C() holds f1.x = F(x)) & (for x
  being Element of C() holds f2.x = F(x)) holds f1 = f2 proof
  let f1,f2 be Function of C(),D() such that
A1: for x being Element of C() holds f1.x = F(x) and
A2: for x being Element of C() holds f2.x = F(x);
  now
    let x be Element of C();
    thus f1.x = F(x) by A1
      .= f2.x by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  BinOpDefuniq{A()->non empty set, O(Element of A(),Element of A())->set}: for
o1,o2 being BinOp of A() st (for a,b being Element of A() holds o1.(a,b) = O(a,
  b)) & (for a,b being Element of A() holds o2.(a,b) = O(a,b)) holds o1 = o2
proof
  let o1,o2 be BinOp of A() such that
A1: for a,b being Element of A() holds o1.(a,b) = O(a,b) and
A2: for a,b being Element of A() holds o2.(a,b) = O(a,b);
  now
    let a,b be Element of A();
    thus o1.(a,b) = O(a,b) by A1
      .= o2.(a,b) by A2;
  end;
  hence thesis by BINOP_1:2;
end;

scheme
  CFuncDefUniq{F(complex number)->set}: for f1,f2 being
Function of COMPLEX,COMPLEX st
   (for x being complex number holds f1.x = F(x)) & (for x
  being complex number holds f2.x = F(x)) holds f1 = f2 proof
  let f1,f2 be Function of COMPLEX,COMPLEX such that
A1: for x being complex number holds f1.x = F(x) and
A2: for x being complex number holds f2.x = F(x);
  now
    let x be Element of COMPLEX;
    thus f1.x = F(x) by A1
      .= f2.x by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  RFuncDefUniq{F(real number)->set}: for f1,f2 being
Function of REAL,REAL st
   (for x being real number holds f1.x = F(x)) & (for x
  being real number holds f2.x = F(x)) holds f1 = f2 proof
  let f1,f2 be Function of REAL,REAL such that
A1: for x being real number holds f1.x = F(x) and
A2: for x being real number holds f2.x = F(x);
  now
    let x be Element of REAL;
    thus f1.x = F(x) by A1
      .= f2.x by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

registration
  cluster -> rational for Element of RAT;
  coherence by RAT_1:def 2;
end;

scheme
  WFuncDefUniq{F(rational number)->set}: for f1,f2 being
Function of RAT,RAT st
   (for x being rational number holds f1.x = F(x)) & (for x
  being rational number holds f2.x = F(x)) holds f1 = f2 proof
  let f1,f2 be Function of RAT,RAT such that
A1: for x being rational number holds f1.x = F(x) and
A2: for x being rational number holds f2.x = F(x);
  now
    let x be Element of RAT;
    thus f1.x = F(x) by A1
      .= f2.x by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  IFuncDefUniq{F(integer number)->set}: for f1,f2 being
Function of INT,INT st
   (for x being integer number holds f1.x = F(x)) & (for x
  being integer number holds f2.x = F(x)) holds f1 = f2 proof
  let f1,f2 be Function of INT,INT such that
A1: for x being integer number holds f1.x = F(x) and
A2: for x being integer number holds f2.x = F(x);
  now
    let x be Element of INT;
    thus f1.x = F(x) by A1
      .= f2.x by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  NFuncDefUniq{F(Nat)->set}: for f1,f2 being
Function of NAT,NAT st
   (for x being Nat holds f1.x = F(x)) & (for x
  being Nat holds f2.x = F(x)) holds f1 = f2 proof
  let f1,f2 be Function of NAT,NAT such that
A1: for x being Nat holds f1.x = F(x) and
A2: for x being Nat holds f2.x = F(x);
  now
    let x be Element of NAT;
    thus f1.x = F(x) by A1
      .= f2.x by A2;
  end;
  hence thesis by FUNCT_2:63;
end;

scheme
  CBinOpDefuniq{O(complex number,complex number)->set}:
  for o1,o2 being BinOp of COMPLEX st
  (for a,b being complex number holds o1.(a,b) = O(a,b)) &
  (for a,b being complex number holds o2.(a,b) = O(a,b)) holds o1 = o2
proof
  let o1,o2 be BinOp of COMPLEX such that
A1: for a,b being complex number holds o1.(a,b) = O(a,b) and
A2: for a,b being complex number holds o2.(a,b) = O(a,b);
  now
    let a,b be Element of COMPLEX;
    thus o1.(a,b) = O(a,b) by A1
      .= o2.(a,b) by A2;
  end;
  hence thesis by BINOP_1:2;
end;

scheme
  RBinOpDefuniq{O(real number,real number)->set}:
  for o1,o2 being BinOp of REAL st
  (for a,b being real number holds o1.(a,b) = O(a,b)) &
  (for a,b being real number holds o2.(a,b) = O(a,b)) holds o1 = o2
proof
  let o1,o2 be BinOp of REAL such that
A1: for a,b being real number holds o1.(a,b) = O(a,b) and
A2: for a,b being real number holds o2.(a,b) = O(a,b);
  now
    let a,b be Element of REAL;
    thus o1.(a,b) = O(a,b) by A1
      .= o2.(a,b) by A2;
  end;
  hence thesis by BINOP_1:2;
end;

scheme
  WBinOpDefuniq{O(rational number,rational number)->set}:
  for o1,o2 being BinOp of RAT st
  (for a,b being rational number holds o1.(a,b) = O(a,b)) &
  (for a,b being rational number holds o2.(a,b) = O(a,b)) holds o1 = o2
proof
  let o1,o2 be BinOp of RAT such that
A1: for a,b being rational number holds o1.(a,b) = O(a,b) and
A2: for a,b being rational number holds o2.(a,b) = O(a,b);
  now
    let a,b be Element of RAT;
    thus o1.(a,b) = O(a,b) by A1
      .= o2.(a,b) by A2;
  end;
  hence thesis by BINOP_1:2;
end;

scheme
  IBinOpDefuniq{O(integer number,integer number)->set}:
  for o1,o2 being BinOp of INT st
  (for a,b being integer number holds o1.(a,b) = O(a,b)) &
  (for a,b being integer number holds o2.(a,b) = O(a,b)) holds o1 = o2
proof
  let o1,o2 be BinOp of INT such that
A1: for a,b being integer number holds o1.(a,b) = O(a,b) and
A2: for a,b being integer number holds o2.(a,b) = O(a,b);
  now
    let a,b be Element of INT;
    thus o1.(a,b) = O(a,b) by A1
      .= o2.(a,b) by A2;
  end;
  hence thesis by BINOP_1:2;
end;

scheme
  NBinOpDefuniq{O(Nat,Nat)->set}:
  for o1,o2 being BinOp of NAT st
  (for a,b being Nat holds o1.(a,b) = O(a,b)) &
  (for a,b being Nat holds o2.(a,b) = O(a,b)) holds o1 = o2
proof
  let o1,o2 be BinOp of NAT such that
A1: for a,b being Nat holds o1.(a,b) = O(a,b) and
A2: for a,b being Nat holds o2.(a,b) = O(a,b);
  now
    let a,b be Element of NAT;
    thus o1.(a,b) = O(a,b) by A1
      .= o2.(a,b) by A2;
  end;
  hence thesis by BINOP_1:2;
end;

scheme
  CLambda2D{F(complex number,complex number) -> complex number}:
 ex f being Function of [:COMPLEX,COMPLEX:],COMPLEX st
  for x,y being complex number holds f.(x,y)=F(x,y)
proof
  defpred P[complex number,complex number,set] means $3 = F($1,$2);
A1: for x,y being Element of COMPLEX ex z being Element of COMPLEX st P[x,y,z]
   proof let x,y being Element of COMPLEX;
    reconsider z = F(x,y) as Element of COMPLEX by XCMPLX_0:def 2;
    take z;
    thus P[x,y,z];
   end;
  consider f being Function of [:COMPLEX,COMPLEX:],COMPLEX such that
A2:   for x,y being Element of COMPLEX
   holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
 take f; let x,y be complex number;
  reconsider x,y as Element of COMPLEX by XCMPLX_0:def 2;
  P[x,y,f.(x,y)] by A2;
  then f.(x,y)=F(x,y);
 hence thesis;
end;

scheme
  RLambda2D{F(real number,real number) -> real number}:
 ex f being Function of [:REAL,REAL:],REAL st
  for x,y being real number holds f.(x,y)=F(x,y)
proof
  defpred P[real number,real number,set] means $3 = F($1,$2);
A1: for x,y being Element of REAL ex z being Element of REAL st P[x,y,z]
   proof let x,y being Element of REAL;
    reconsider z = F(x,y) as Element of REAL by XREAL_0:def 1;
    take z;
    thus P[x,y,z];
   end;
  consider f being Function of [:REAL,REAL:],REAL such that
A2:   for x,y being Element of REAL holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1
);
 take f; let x,y be real number;
  reconsider x,y as Element of REAL by XREAL_0:def 1;
  P[x,y,f.(x,y)] by A2;
  then f.(x,y)=F(x,y);
 hence thesis;
end;

scheme
  WLambda2D{F(rational number,rational number) -> rational number}:
 ex f being Function of [:RAT,RAT:],RAT st
  for x,y being rational number holds f.(x,y)=F(x,y)
proof
  defpred P[rational number,rational number,set] means $3 = F($1,$2);
A1: for x,y being Element of RAT ex z being Element of RAT st P[x,y,z]
   proof let x,y being Element of RAT;
    reconsider z = F(x,y) as Element of RAT by RAT_1:def 2;
    take z;
    thus P[x,y,z];
   end;
  consider f being Function of [:RAT,RAT:],RAT such that
A2:   for x,y being Element of RAT holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
 take f; let x,y be rational number;
  reconsider x,y as Element of RAT by RAT_1:def 2;
  P[x,y,f.(x,y)] by A2;
  then f.(x,y)=F(x,y);
 hence thesis;
end;

scheme
  ILambda2D{F(integer number,integer number) -> integer number}:
 ex f being Function of [:INT,INT:],INT st
  for x,y being integer number holds f.(x,y)=F(x,y)
proof
  defpred P[integer number,integer number,set] means $3 = F($1,$2);
A1: for x,y being Element of INT ex z being Element of INT st P[x,y,z]
   proof let x,y being Element of INT;
    reconsider z = F(x,y) as Element of INT by INT_1:def 2;
    take z;
    thus P[x,y,z];
   end;
  consider f being Function of [:INT,INT:],INT such that
A2:   for x,y being Element of INT holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
 take f; let x,y be integer number;
  reconsider x,y as Element of INT by INT_1:def 2;
  P[x,y,f.(x,y)] by A2;
  then f.(x,y)=F(x,y);
 hence thesis;
end;

scheme
  NLambda2D{F(Nat,Nat) -> Nat}:
 ex f being Function of [:NAT,NAT:],NAT st
  for x,y being Nat holds f.(x,y)=F(x,y)
proof
  defpred P[Nat,Nat,set] means $3 = F($1,$2);
A1: for x,y being Element of NAT ex z being Element of NAT st P[x,y,z]
   proof let x,y being Element of NAT;
    reconsider z = F(x,y) as Element of NAT by ORDINAL1:def 12;
    take z;
    thus P[x,y,z];
   end;
  consider f being Function of [:NAT,NAT:],NAT such that
A2:   for x,y being Element of NAT holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
 take f; let x,y be Nat;
  reconsider x,y as Element of NAT by ORDINAL1:def 12;
  P[x,y,f.(x,y)] by A2;
  then f.(x,y)=F(x,y);
 hence thesis;
end;

scheme
  CLambdaD{F(complex number) -> complex number }: ex f
being Function of COMPLEX,COMPLEX st
 for x being complex number holds f.x = F(x)
proof
  defpred P[Element of COMPLEX,set] means $2 = F($1);
A1: for x being Element of COMPLEX ex y being Element of COMPLEX st P[x,y]
  proof let x being Element of COMPLEX;
    reconsider y = F(x) as Element of COMPLEX by XCMPLX_0:def 2;
   take y;
   thus P[x,y];
  end;
  consider f being Function of COMPLEX,COMPLEX such that
A2: for x being Element of COMPLEX holds P[x,f.x] from FUNCT_2:sch 3(A1);
 take f; let c be complex number;
  reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
  P[c,f.c] by A2;
 hence thesis;
end;

scheme
  RLambdaD{F(real number) -> real number }: ex f
being Function of REAL,REAL st
 for x being real number holds f.x = F(x)
proof
  defpred P[Element of REAL,set] means $2 = F($1);
A1: for x being Element of REAL ex y being Element of REAL st P[x,y]
  proof let x being Element of REAL;
    reconsider y = F(x) as Element of REAL by XREAL_0:def 1;
   take y;
   thus P[x,y];
  end;
  consider f being Function of REAL,REAL such that
A2: for x being Element of REAL holds P[x,f.x] from FUNCT_2:sch 3(A1);
 take f; let c be real number;
  reconsider c as Element of REAL by XREAL_0:def 1;
  P[c,f.c] by A2;
 hence thesis;
end;

scheme
  WLambdaD{F(rational number) -> rational number }: ex f
being Function of RAT,RAT st
 for x being rational number holds f.x = F(x)
proof
  defpred P[Element of RAT,set] means $2 = F($1);
A1: for x being Element of RAT ex y being Element of RAT st P[x,y]
  proof let x being Element of RAT;
    reconsider y = F(x) as Element of RAT by RAT_1:def 2;
   take y;
   thus P[x,y];
  end;
  consider f being Function of RAT,RAT such that
A2: for x being Element of RAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
 take f; let c be rational number;
  reconsider c as Element of RAT by RAT_1:def 2;
  P[c,f.c] by A2;
 hence thesis;
end;

scheme
  ILambdaD{F(integer number) -> integer number }: ex f
being Function of INT,INT st
 for x being integer number holds f.x = F(x)
proof
  defpred P[Element of INT,set] means $2 = F($1);
A1: for x being Element of INT ex y being Element of INT st P[x,y]
  proof let x being Element of INT;
    reconsider y = F(x) as Element of INT by INT_1:def 2;
   take y;
   thus P[x,y];
  end;
  consider f being Function of INT,INT such that
A2: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1);
 take f; let c be integer number;
  reconsider c as Element of INT by INT_1:def 2;
  P[c,f.c] by A2;
 hence thesis;
end;

scheme
  NLambdaD{F(Nat) -> Nat }: ex f
being Function of NAT,NAT st
 for x being Nat holds f.x = F(x)
proof
  defpred P[Element of NAT,set] means $2 = F($1);
A1: for x being Element of NAT ex y being Element of NAT st P[x,y]
  proof let x being Element of NAT;
    reconsider y = F(x) as Element of NAT by ORDINAL1:def 12;
   take y;
   thus P[x,y];
  end;
  consider f being Function of NAT,NAT such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
 take f; let c be Nat;
  reconsider c as Element of NAT by ORDINAL1:def 12;
  P[c,f.c] by A2;
 hence thesis;
end;

reserve c,c1,c2 for complex number;

definition
  let c1;
  redefine func -c1 -> Element of COMPLEX;
  coherence by XCMPLX_0:def 2;
  redefine func c1" -> Element of COMPLEX;
  coherence by XCMPLX_0:def 2;
  let c2;
  redefine func c1+c2 -> Element of COMPLEX;
  coherence by XCMPLX_0:def 2;
  redefine func c1-c2 -> Element of COMPLEX;
  coherence by XCMPLX_0:def 2;
  redefine func c1*c2 -> Element of COMPLEX;
  coherence by XCMPLX_0:def 2;
  redefine func c1/c2 -> Element of COMPLEX;
  coherence by XCMPLX_0:def 2;
end;

reserve r,r1,r2 for real number;

definition
  let r1;
  redefine func -r1 -> Element of REAL;
  coherence by XREAL_0:def 1;
  redefine func r1" -> Element of REAL;
  coherence by XREAL_0:def 1;
  let r2;
  redefine func r1+r2 -> Element of REAL;
  coherence by XREAL_0:def 1;
  redefine func r1-r2 -> Element of REAL;
  coherence by XREAL_0:def 1;
  redefine func r1*r2 -> Element of REAL;
  coherence by XREAL_0:def 1;
  redefine func r1/r2 -> Element of REAL;
  coherence by XREAL_0:def 1;
end;

reserve w,w1,w2 for rational number;

definition
  let w1;
  redefine func -w1 -> Element of RAT;
  coherence by RAT_1:def 2;
  redefine func w1" -> Element of RAT;
  coherence by RAT_1:def 2;
  let w2;
  redefine func w1+w2 -> Element of RAT;
  coherence by RAT_1:def 2;
  redefine func w1-w2 -> Element of RAT;
  coherence by RAT_1:def 2;
  redefine func w1*w2 -> Element of RAT;
  coherence by RAT_1:def 2;
  redefine func w1/w2 -> Element of RAT;
  coherence by RAT_1:def 2;
end;

reserve i,i1,i2 for integer number;

definition
  let i1;
  redefine func -i1 -> Element of INT;
  coherence by INT_1:def 2;
  let i2;
  redefine func i1+i2 -> Element of INT;
  coherence by INT_1:def 2;
  redefine func i1-i2 -> Element of INT;
  coherence by INT_1:def 2;
  redefine func i1*i2 -> Element of INT;
  coherence by INT_1:def 2;
end;

reserve n1,n2 for Nat;

definition
  let n1,n2;
  redefine func n1+n2 -> Element of NAT;
  coherence by ORDINAL1:def 12;
  redefine func n1*n2 -> Element of NAT;
  coherence by ORDINAL1:def 12;
end;

definition
  func compcomplex -> UnOp of COMPLEX means
  for c holds it.c = -c;
  existence from CLambdaD;
  uniqueness from CFuncDefUniq;
  func invcomplex -> UnOp of COMPLEX means
  for c holds it.c = c";
  existence from CLambdaD;
  uniqueness from CFuncDefUniq;
  func addcomplex -> BinOp of COMPLEX means
  :Def3:
  for c1,c2 holds it.(c1,c2) = c1 + c2;
  existence from CLambda2D;
  uniqueness from CBinOpDefuniq;
  func diffcomplex -> BinOp of COMPLEX means
  for c1,c2 holds it.(c1,c2) = c1 - c2;
  existence from CLambda2D;
  uniqueness from CBinOpDefuniq;
  func multcomplex -> BinOp of COMPLEX means
  :Def5:
  for c1,c2 holds it.(c1,c2) = c1 * c2;
  existence from CLambda2D;
  uniqueness from CBinOpDefuniq;
  func divcomplex -> BinOp of COMPLEX means
  for c1,c2 holds it.(c1,c2) = c1 / c2;
  existence from CLambda2D;
  uniqueness from CBinOpDefuniq;
end;

definition
  func compreal -> UnOp of REAL means
  for r holds it.r = -r;
  existence from RLambdaD;
  uniqueness from RFuncDefUniq;
  func invreal -> UnOp of REAL means
  for r holds it.r = r";
  existence from RLambdaD;
  uniqueness from RFuncDefUniq;
  func addreal -> BinOp of REAL means
  :Def9:
  for r1,r2 holds it.(r1,r2) = r1 + r2;
  existence from RLambda2D;
  uniqueness from RBinOpDefuniq;
  func diffreal -> BinOp of REAL means
  for r1,r2 holds it.(r1,r2) = r1 - r2;
  existence from RLambda2D;
  uniqueness from RBinOpDefuniq;
  func multreal -> BinOp of REAL means
  :Def11:
  for r1,r2 holds it.(r1,r2) = r1 * r2;
  existence from RLambda2D;
  uniqueness from RBinOpDefuniq;
  func divreal -> BinOp of REAL means
  for r1,r2 holds it.(r1,r2) = r1 / r2;
  existence from RLambda2D;
  uniqueness from RBinOpDefuniq;
end;

definition
  func comprat -> UnOp of RAT means
  for w holds it.w = -w;
  existence from WLambdaD;
  uniqueness from WFuncDefUniq;
  func invrat -> UnOp of RAT means
  for w holds it.w = w";
  existence from WLambdaD;
  uniqueness from WFuncDefUniq;
  func addrat -> BinOp of RAT means
  :Def15:
  for w1,w2 holds it.(w1,w2) = w1 + w2;
  existence from WLambda2D;
  uniqueness from WBinOpDefuniq;
  func diffrat -> BinOp of RAT means
  for w1,w2 holds it.(w1,w2) = w1 - w2;
  existence from WLambda2D;
  uniqueness from WBinOpDefuniq;
  func multrat -> BinOp of RAT means
  :Def17:
  for w1,w2 holds it.(w1,w2) = w1 * w2;
  existence from WLambda2D;
  uniqueness from WBinOpDefuniq;
  func divrat -> BinOp of RAT means
  for w1,w2 holds it.(w1,w2) = w1 / w2;
  existence from WLambda2D;
  uniqueness from WBinOpDefuniq;
end;

definition
  func compint -> UnOp of INT means
  for i holds it.i = -i;
  existence from ILambdaD;
  uniqueness from IFuncDefUniq;
  func addint -> BinOp of INT means
  :Def20:
  for i1,i2 holds it.(i1,i2) = i1 + i2;
  existence from ILambda2D;
  uniqueness from IBinOpDefuniq;
  func diffint -> BinOp of INT means
  for i1,i2 holds it.(i1,i2) = i1 - i2;
  existence from ILambda2D;
  uniqueness from IBinOpDefuniq;
  func multint -> BinOp of INT means
  :Def22:
  for i1,i2 holds it.(i1,i2) = i1 * i2;
  existence from ILambda2D;
  uniqueness from IBinOpDefuniq;
end;

definition
  func addnat -> BinOp of NAT means
  :Def23:
  for n1,n2 holds it.(n1,n2) = n1 + n2;
  existence from NLambda2D;
  uniqueness from NBinOpDefuniq;
  func multnat -> BinOp of NAT means
  :Def24:
  for n1,n2 holds it.(n1,n2) = n1 * n2;
  existence from NLambda2D;
  uniqueness from NBinOpDefuniq;
end;

registration
  cluster addcomplex -> commutative associative;
  coherence
  proof
    thus addcomplex is commutative
    proof
      let c1,c2 be Element of COMPLEX;
      thus addcomplex.(c1,c2) = c1 + c2 by Def3
        .= addcomplex.(c2,c1) by Def3;
    end;
    let c1,c2,c3 be Element of COMPLEX;
    thus addcomplex.(c1,addcomplex.(c2,c3)) = c1 + addcomplex.(c2,c3) by Def3
      .= c1 + (c2 + c3) by Def3
      .= c1 + c2 + c3
      .= addcomplex.(c1,c2) + c3 by Def3
      .= addcomplex.(addcomplex.(c1,c2),c3) by Def3;
  end;
  cluster multcomplex -> commutative associative;
  coherence
  proof
    thus multcomplex is commutative
    proof
      let c1,c2 be Element of COMPLEX;
      thus multcomplex.(c1,c2) = c1 * c2 by Def5
        .= multcomplex.(c2,c1) by Def5;
    end;
    let c1,c2,c3 be Element of COMPLEX;
    thus multcomplex.(c1,multcomplex.(c2,c3)) = c1 * multcomplex.(c2,c3) by
Def5
      .= c1 * (c2 * c3) by Def5
      .= c1 * c2 * c3
      .= multcomplex.(c1,c2) * c3 by Def5
      .= multcomplex.(multcomplex.(c1,c2),c3) by Def5;
  end;
  cluster addreal -> commutative associative;
  coherence
  proof
    thus addreal is commutative
    proof
      let r1,r2 be Element of REAL;
      thus addreal.(r1,r2) = r1 + r2 by Def9
        .= addreal.(r2,r1) by Def9;
    end;
    let r1,r2,r3 be Element of REAL;
    thus addreal.(r1,addreal.(r2,r3)) = r1 + addreal.(r2,r3) by Def9
      .= r1 + (r2 + r3) by Def9
      .= r1 + r2 + r3
      .= addreal.(r1,r2) + r3 by Def9
      .= addreal.(addreal.(r1,r2),r3) by Def9;
  end;
  cluster multreal -> commutative associative;
  coherence
  proof
    thus multreal is commutative
    proof
      let r1,r2 be Element of REAL;
      thus multreal.(r1,r2) = r1 * r2 by Def11
        .= multreal.(r2,r1) by Def11;
    end;
    let r1,r2,r3 be Element of REAL;
    thus multreal.(r1,multreal.(r2,r3)) = r1 * multreal.(r2,r3) by Def11
      .= r1 * (r2 * r3) by Def11
      .= r1 * r2 * r3
      .= multreal.(r1,r2) * r3 by Def11
      .= multreal.(multreal.(r1,r2),r3) by Def11;
  end;
  cluster addrat -> commutative associative;
  coherence
  proof
    thus addrat is commutative
    proof
      let w1,w2 be Element of RAT;
      thus addrat.(w1,w2) = w1 + w2 by Def15
        .= addrat.(w2,w1) by Def15;
    end;
    let w1,w2,w3 be Element of RAT;
    thus addrat.(w1,addrat.(w2,w3)) = w1 + addrat.(w2,w3) by Def15
      .= w1 + (w2 + w3) by Def15
      .= w1 + w2 + w3
      .= addrat.(w1,w2) + w3 by Def15
      .= addrat.(addrat.(w1,w2),w3) by Def15;
  end;
  cluster multrat -> commutative associative;
  coherence
  proof
    thus multrat is commutative
    proof
      let w1,w2 be Element of RAT;
      thus multrat.(w1,w2) = w1 * w2 by Def17
        .= multrat.(w2,w1) by Def17;
    end;
    let w1,w2,w3 be Element of RAT;
    thus multrat.(w1,multrat.(w2,w3)) = w1 * multrat.(w2,w3) by Def17
      .= w1 * (w2 * w3) by Def17
      .= w1 * w2 * w3
      .= multrat.(w1,w2) * w3 by Def17
      .= multrat.(multrat.(w1,w2),w3) by Def17;
  end;
  cluster addint -> commutative associative;
  coherence
  proof
    thus addint is commutative
    proof
      let i1,i2 be Element of INT;
      thus addint.(i1,i2) = i1 + i2 by Def20
        .= addint.(i2,i1) by Def20;
    end;
    let i1,i2,i3 be Element of INT;
    thus addint.(i1,addint.(i2,i3)) = i1 + addint.(i2,i3) by Def20
      .= i1 + (i2 + i3) by Def20
      .= i1 + i2 + i3
      .= addint.(i1,i2) + i3 by Def20
      .= addint.(addint.(i1,i2),i3) by Def20;
  end;
  cluster multint -> commutative associative;
  coherence
  proof
    thus multint is commutative
    proof
      let i1,i2 be Element of INT;
      thus multint.(i1,i2) = i1 * i2 by Def22
        .= multint.(i2,i1) by Def22;
    end;
    let i1,i2,i3 be Element of INT;
    thus multint.(i1,multint.(i2,i3)) = i1 * multint.(i2,i3) by Def22
      .= i1 * (i2 * i3) by Def22
      .= i1 * i2 * i3
      .= multint.(i1,i2) * i3 by Def22
      .= multint.(multint.(i1,i2),i3) by Def22;
  end;
  cluster addnat -> commutative associative;
  coherence
  proof
    thus addnat is commutative
    proof
      let n1,n2 be Element of NAT;
      thus addnat.(n1,n2) = n1 + n2 by Def23
        .= addnat.(n2,n1) by Def23;
    end;
    let n1,n2,n3 be Element of NAT;
    thus addnat.(n1,addnat.(n2,n3)) = n1 + addnat.(n2,n3) by Def23
      .= n1 + (n2 + n3) by Def23
      .= n1 + n2 + n3
      .= addnat.(n1,n2) + n3 by Def23
      .= addnat.(addnat.(n1,n2),n3) by Def23;
  end;
  cluster multnat -> commutative associative;
  coherence
  proof
    thus multnat is commutative
    proof
      let n1,n2 be Element of NAT;
      thus multnat.(n1,n2) = n1 * n2 by Def24
        .= multnat.(n2,n1) by Def24;
    end;
    let n1,n2,n3 be Element of NAT;
    thus multnat.(n1,multnat.(n2,n3)) = n1 * multnat.(n2,n3) by Def24
      .= n1 * (n2 * n3) by Def24
      .= n1 * n2 * n3
      .= multnat.(n1,n2) * n3 by Def24
      .= multnat.(multnat.(n1,n2),n3) by Def24;
  end;
end;

Lm1: 0 in NAT;

then reconsider z = 0 as Element of COMPLEX by NUMBERS:20;

Lm2: z is_a_unity_wrt addcomplex
proof
  thus for c being Element of COMPLEX holds addcomplex.(z,c) = c
  proof
    let c be Element of COMPLEX;
    thus addcomplex.(z,c) = 0 + c by Def3
      .= c;
  end;
  let c be Element of COMPLEX;
  thus addcomplex.(c,z) = c + 0 by Def3
    .= c;
end;

Lm3: 0 is_a_unity_wrt addreal
proof
  thus for r being Element of REAL holds addreal.(0,r) = r
  proof
    let r be Element of REAL;
    thus addreal.(0,r) = 0 + r by Def9
      .= r;
  end;
  let r be Element of REAL;
  thus addreal.(r,0) = r + 0 by Def9
    .= r;
end;

reconsider z = 0 as Element of RAT by Lm1,NUMBERS:18;

Lm4: z is_a_unity_wrt addrat
proof
  thus for w being Element of RAT holds addrat.(z,w) = w
  proof
    let w be Element of RAT;
    thus addrat.(z,w) = 0 + w by Def15
      .= w;
  end;
  let w be Element of RAT;
  thus addrat.(w,z) = w + 0 by Def15
    .= w;
end;

reconsider z = 0 as Element of INT by Lm1,NUMBERS:17;

Lm5: z is_a_unity_wrt addint
proof
  thus for i being Element of INT holds addint.(z,i) = i
  proof
    let i be Element of INT;
    thus addint.(z,i) = 0 + i by Def20
      .= i;
  end;
  let i be Element of INT;
  thus addint.(i,z) = i + 0 by Def20
    .= i;
end;

Lm6: 0 is_a_unity_wrt addnat
proof
  thus for n being Element of NAT holds addnat.(0,n) = n
  proof
    let n be Element of NAT;
    thus addnat.(0,n) = 0 + n by Def23
      .= n;
  end;
  let n be Element of NAT;
  thus addnat.(n,0) = n + 0 by Def23
    .= n;
end;

Lm7: 1 in NAT;

then reconsider z = 1 as Element of COMPLEX by NUMBERS:20;

Lm8: z is_a_unity_wrt multcomplex
proof
  thus for c being Element of COMPLEX holds multcomplex.(z,c) = c
  proof
    let c be Element of COMPLEX;
    thus multcomplex.(z,c) = 1 * c by Def5
      .= c;
  end;
  let c be Element of COMPLEX;
  thus multcomplex.(c,z) = c * 1 by Def5
    .= c;
end;

Lm9: 1 is_a_unity_wrt multreal
proof
  thus for r being Element of REAL holds multreal.(1,r) = r
  proof
    let r be Element of REAL;
    thus multreal.(1,r) = 1 * r by Def11
      .= r;
  end;
  let r be Element of REAL;
  thus multreal.(r,1) = r * 1 by Def11
    .= r;
end;

reconsider z = 1 as Element of RAT by Lm7,NUMBERS:18;

Lm10: z is_a_unity_wrt multrat
proof
  thus for w being Element of RAT holds multrat.(z,w) = w
  proof
    let w be Element of RAT;
    thus multrat.(z,w) = 1 * w by Def17
      .= w;
  end;
  let w be Element of RAT;
  thus multrat.(w,z) = w * 1 by Def17
    .= w;
end;

reconsider z = 1 as Element of INT by Lm7,NUMBERS:17;

Lm11: z is_a_unity_wrt multint
proof
  thus for i being Element of INT holds multint.(z,i) = i
  proof
    let i be Element of INT;
    thus multint.(z,i) = 1 * i by Def22
      .= i;
  end;
  let i be Element of INT;
  thus multint.(i,z) = i * 1 by Def22
    .= i;
end;

Lm12: 1 is_a_unity_wrt multnat
proof
  thus for n being Element of NAT holds multnat.(1,n) = n
  proof
    let n be Element of NAT;
    thus multnat.(1,n) = 1 * n by Def24
      .= n;
  end;
  let n be Element of NAT;
  thus multnat.(n,1) = n * 1 by Def24
    .= n;
end;

registration
  cluster addcomplex -> having_a_unity;
  coherence by Lm2,SETWISEO:def 2;
  cluster addreal -> having_a_unity;
  coherence by Lm3,SETWISEO:def 2;
  cluster addrat -> having_a_unity;
  coherence by Lm4,SETWISEO:def 2;
  cluster addint -> having_a_unity;
  coherence by Lm5,SETWISEO:def 2;
  cluster addnat -> having_a_unity;
  coherence by Lm6,SETWISEO:def 2;
  cluster multcomplex -> having_a_unity;
  coherence by Lm8,SETWISEO:def 2;
  cluster multreal -> having_a_unity;
  coherence by Lm9,SETWISEO:def 2;
  cluster multrat -> having_a_unity;
  coherence by Lm10,SETWISEO:def 2;
  cluster multint -> having_a_unity;
  coherence by Lm11,SETWISEO:def 2;
  cluster multnat -> having_a_unity;
  coherence by Lm12,SETWISEO:def 2;
end;

theorem
  the_unity_wrt addcomplex = 0 by Lm2,BINOP_1:def 8;

theorem
  the_unity_wrt addreal = 0 by Lm3,BINOP_1:def 8;

theorem
  the_unity_wrt addrat = 0 by Lm4,BINOP_1:def 8;

theorem
  the_unity_wrt addint = 0 by Lm5,BINOP_1:def 8;

theorem
  the_unity_wrt addnat = 0 by Lm6,BINOP_1:def 8;

theorem
  the_unity_wrt multcomplex = 1 by Lm8,BINOP_1:def 8;

theorem
  the_unity_wrt multreal = 1 by Lm9,BINOP_1:def 8;

theorem
  the_unity_wrt multrat = 1 by Lm10,BINOP_1:def 8;

theorem
  the_unity_wrt multint = 1 by Lm11,BINOP_1:def 8;

theorem
  the_unity_wrt multnat = 1 by Lm12,BINOP_1:def 8;