:: Binary Operations on Numbers
:: by Library Committee
::
:: Received June 21, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

scheme :: BINOP_2:sch 1
FuncDefUniq{ F₁() -> non empty set , F₂() -> non empty set , F₃( Element of F₁()) -> object } :

for f1, f2 being Function of F₁(),F₂() st ( for x being Element of F₁() holds f1 . x = F₃(x) ) & ( for x being Element of F₁() holds f2 . x = F₃(x) ) holds
f1 = f2

proof end;

scheme :: BINOP_2:sch 2
BinOpDefuniq{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁()) -> object } :

for o1, o2 being BinOp of F₁() st ( for a, b being Element of F₁() holds o1 . (a,b) = F₂(a,b) ) & ( for a, b being Element of F₁() holds o2 . (a,b) = F₂(a,b) ) holds
o1 = o2

proof end;

scheme :: BINOP_2:sch 3
CFuncDefUniq{ F₁( object ) -> object } :

for f1, f2 being Function of COMPLEX,COMPLEX st ( for x being Complex holds f1 . x = F₁(x) ) & ( for x being Complex holds f2 . x = F₁(x) ) holds
f1 = f2

proof end;

scheme :: BINOP_2:sch 4
RFuncDefUniq{ F₁( Real) -> object } :

for f1, f2 being Function of REAL,REAL st ( for x being Real holds f1 . x = F₁(x) ) & ( for x being Real holds f2 . x = F₁(x) ) holds
f1 = f2

proof end;

registration

cluster -> rational for Element of RAT ;

coherence
for b₁ being Element of RAT holds b₁ is rational by RAT_1:def 2;

end;

scheme :: BINOP_2:sch 5
WFuncDefUniq{ F₁( Rational) -> object } :

for f1, f2 being Function of RAT,RAT st ( for x being Rational holds f1 . x = F₁(x) ) & ( for x being Rational holds f2 . x = F₁(x) ) holds
f1 = f2

proof end;

scheme :: BINOP_2:sch 6
IFuncDefUniq{ F₁( Integer) -> object } :

for f1, f2 being Function of INT,INT st ( for x being Integer holds f1 . x = F₁(x) ) & ( for x being Integer holds f2 . x = F₁(x) ) holds
f1 = f2

proof end;

scheme :: BINOP_2:sch 7
NFuncDefUniq{ F₁( Nat) -> object } :

for f1, f2 being sequence of NAT st ( for x being Nat holds f1 . x = F₁(x) ) & ( for x being Nat holds f2 . x = F₁(x) ) holds
f1 = f2

proof end;

scheme :: BINOP_2:sch 8
CBinOpDefuniq{ F₁( Complex, Complex) -> object } :

for o1, o2 being BinOp of COMPLEX st ( for a, b being Complex holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Complex holds o2 . (a,b) = F₁(a,b) ) holds
o1 = o2

proof end;

scheme :: BINOP_2:sch 9
RBinOpDefuniq{ F₁( Real, Real) -> object } :

for o1, o2 being BinOp of REAL st ( for a, b being Real holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Real holds o2 . (a,b) = F₁(a,b) ) holds
o1 = o2

proof end;

scheme :: BINOP_2:sch 10
WBinOpDefuniq{ F₁( Rational, Rational) -> object } :

for o1, o2 being BinOp of RAT st ( for a, b being Rational holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Rational holds o2 . (a,b) = F₁(a,b) ) holds
o1 = o2

proof end;

scheme :: BINOP_2:sch 11
IBinOpDefuniq{ F₁( Integer, Integer) -> object } :

for o1, o2 being BinOp of INT st ( for a, b being Integer holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Integer holds o2 . (a,b) = F₁(a,b) ) holds
o1 = o2

proof end;

scheme :: BINOP_2:sch 12
NBinOpDefuniq{ F₁( Nat, Nat) -> object } :

for o1, o2 being BinOp of NAT st ( for a, b being Nat holds o1 . (a,b) = F₁(a,b) ) & ( for a, b being Nat holds o2 . (a,b) = F₁(a,b) ) holds
o1 = o2

proof end;

scheme :: BINOP_2:sch 13
CLambda2D{ F₁( Complex, Complex) -> Complex } :

ex f being Function of [:COMPLEX,COMPLEX:],COMPLEX st
for x, y being Complex holds f . (x,y) = F₁(x,y)

proof end;

scheme :: BINOP_2:sch 14
RLambda2D{ F₁( Real, Real) -> Real } :

ex f being Function of [:REAL,REAL:],REAL st
for x, y being Real holds f . (x,y) = F₁(x,y)

proof end;

scheme :: BINOP_2:sch 15
WLambda2D{ F₁( Rational, Rational) -> Rational } :

ex f being Function of [:RAT,RAT:],RAT st
for x, y being Rational holds f . (x,y) = F₁(x,y)

proof end;

scheme :: BINOP_2:sch 16
ILambda2D{ F₁( Integer, Integer) -> Integer } :

ex f being Function of [:INT,INT:],INT st
for x, y being Integer holds f . (x,y) = F₁(x,y)

proof end;

scheme :: BINOP_2:sch 17
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 end;

scheme :: BINOP_2:sch 18
CLambdaD{ F₁( Complex) -> Complex } :

ex f being Function of COMPLEX,COMPLEX st
for x being Complex holds f . x = F₁(x)

proof end;

scheme :: BINOP_2:sch 19
RLambdaD{ F₁( Real) -> Real } :

ex f being Function of REAL,REAL st
for x being Real holds f . x = F₁(x)

proof end;

scheme :: BINOP_2:sch 20
WLambdaD{ F₁( Rational) -> Rational } :

ex f being Function of RAT,RAT st
for x being Rational holds f . x = F₁(x)

proof end;

scheme :: BINOP_2:sch 21
ILambdaD{ F₁( Integer) -> Integer } :

ex f being Function of INT,INT st
for x being Integer holds f . x = F₁(x)

proof end;

scheme :: BINOP_2:sch 22
NLambdaD{ F₁( Nat) -> Nat } :

ex f being sequence of NAT st
for x being Nat holds f . x = F₁(x)

proof end;

:: 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 :: BINOP_2:def 1
for c being Complex holds it . c = - c;

existence
ex b₁ being UnOp of COMPLEX st
for c being Complex holds b₁ . c = - c from BINOP_2:sch 18();
uniqueness
for b₁, b₂ being UnOp of COMPLEX st ( for c being Complex holds b₁ . c = - c ) & ( for c being Complex holds b₂ . c = - c ) holds
b₁ = b₂ from BINOP_2:sch 3();

func invcomplex -> UnOp of COMPLEX means :: BINOP_2:def 2
for c being Complex holds it . c = c " ;

existence
ex b₁ being UnOp of COMPLEX st
for c being Complex holds b₁ . c = c " from BINOP_2:sch 18();
uniqueness
for b₁, b₂ being UnOp of COMPLEX st ( for c being Complex holds b₁ . c = c " ) & ( for c being Complex holds b₂ . c = c " ) holds
b₁ = b₂ from BINOP_2:sch 3();

func addcomplex -> BinOp of COMPLEX means :Def3: :: BINOP_2:def 3
for c1, c2 being Complex holds it . (c1,c2) = c1 + c2;

existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Complex holds b₁ . (c1,c2) = c1 + c2 from BINOP_2:sch 13();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Complex holds b₁ . (c1,c2) = c1 + c2 ) & ( for c1, c2 being Complex holds b₂ . (c1,c2) = c1 + c2 ) holds
b₁ = b₂ from BINOP_2:sch 8();

func diffcomplex -> BinOp of COMPLEX means :: BINOP_2:def 4
for c1, c2 being Complex holds it . (c1,c2) = c1 - c2;

existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Complex holds b₁ . (c1,c2) = c1 - c2 from BINOP_2:sch 13();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Complex holds b₁ . (c1,c2) = c1 - c2 ) & ( for c1, c2 being Complex holds b₂ . (c1,c2) = c1 - c2 ) holds
b₁ = b₂ from BINOP_2:sch 8();

func multcomplex -> BinOp of COMPLEX means :Def5: :: BINOP_2:def 5
for c1, c2 being Complex holds it . (c1,c2) = c1 * c2;

existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Complex holds b₁ . (c1,c2) = c1 * c2 from BINOP_2:sch 13();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Complex holds b₁ . (c1,c2) = c1 * c2 ) & ( for c1, c2 being Complex holds b₂ . (c1,c2) = c1 * c2 ) holds
b₁ = b₂ from BINOP_2:sch 8();

func divcomplex -> BinOp of COMPLEX means :: BINOP_2:def 6
for c1, c2 being Complex holds it . (c1,c2) = c1 / c2;

existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Complex holds b₁ . (c1,c2) = c1 / c2 from BINOP_2:sch 13();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Complex holds b₁ . (c1,c2) = c1 / c2 ) & ( for c1, c2 being Complex holds b₂ . (c1,c2) = c1 / c2 ) holds
b₁ = b₂ from BINOP_2:sch 8();

end;

:: deftheorem defines compcomplex BINOP_2:def 1 :
for b₁ being UnOp of COMPLEX holds
( b₁ = compcomplex iff for c being Complex holds b₁ . c = - c );

:: deftheorem defines invcomplex BINOP_2:def 2 :
for b₁ being UnOp of COMPLEX holds
( b₁ = invcomplex iff for c being Complex holds b₁ . c = c " );

:: deftheorem Def3 defines addcomplex BINOP_2:def 3 :
for b₁ being BinOp of COMPLEX holds
( b₁ = addcomplex iff for c1, c2 being Complex holds b₁ . (c1,c2) = c1 + c2 );

:: deftheorem defines diffcomplex BINOP_2:def 4 :
for b₁ being BinOp of COMPLEX holds
( b₁ = diffcomplex iff for c1, c2 being Complex holds b₁ . (c1,c2) = c1 - c2 );

:: deftheorem Def5 defines multcomplex BINOP_2:def 5 :
for b₁ being BinOp of COMPLEX holds
( b₁ = multcomplex iff for c1, c2 being Complex holds b₁ . (c1,c2) = c1 * c2 );

:: deftheorem defines divcomplex BINOP_2:def 6 :
for b₁ being BinOp of COMPLEX holds
( b₁ = divcomplex iff for c1, c2 being Complex holds b₁ . (c1,c2) = c1 / c2 );

definition

func compreal -> UnOp of REAL means :: BINOP_2:def 7
for r being Real holds it . r = - r;

existence
ex b₁ being UnOp of REAL st
for r being Real holds b₁ . r = - r from BINOP_2:sch 19();
uniqueness
for b₁, b₂ being UnOp of REAL st ( for r being Real holds b₁ . r = - r ) & ( for r being Real holds b₂ . r = - r ) holds
b₁ = b₂ from BINOP_2:sch 4();

func invreal -> UnOp of REAL means :: BINOP_2:def 8
for r being Real holds it . r = r " ;

existence
ex b₁ being UnOp of REAL st
for r being Real holds b₁ . r = r " from BINOP_2:sch 19();
uniqueness
for b₁, b₂ being UnOp of REAL st ( for r being Real holds b₁ . r = r " ) & ( for r being Real holds b₂ . r = r " ) holds
b₁ = b₂ from BINOP_2:sch 4();

func addreal -> BinOp of REAL means :Def9: :: BINOP_2:def 9
for r1, r2 being Real holds it . (r1,r2) = r1 + r2;

existence
ex b₁ being BinOp of REAL st
for r1, r2 being Real holds b₁ . (r1,r2) = r1 + r2 from BINOP_2:sch 14();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Real holds b₁ . (r1,r2) = r1 + r2 ) & ( for r1, r2 being Real holds b₂ . (r1,r2) = r1 + r2 ) holds
b₁ = b₂ from BINOP_2:sch 9();

func diffreal -> BinOp of REAL means :: BINOP_2:def 10
for r1, r2 being Real holds it . (r1,r2) = r1 - r2;

existence
ex b₁ being BinOp of REAL st
for r1, r2 being Real holds b₁ . (r1,r2) = r1 - r2 from BINOP_2:sch 14();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Real holds b₁ . (r1,r2) = r1 - r2 ) & ( for r1, r2 being Real holds b₂ . (r1,r2) = r1 - r2 ) holds
b₁ = b₂ from BINOP_2:sch 9();

func multreal -> BinOp of REAL means :Def11: :: BINOP_2:def 11
for r1, r2 being Real holds it . (r1,r2) = r1 * r2;

existence
ex b₁ being BinOp of REAL st
for r1, r2 being Real holds b₁ . (r1,r2) = r1 * r2 from BINOP_2:sch 14();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Real holds b₁ . (r1,r2) = r1 * r2 ) & ( for r1, r2 being Real holds b₂ . (r1,r2) = r1 * r2 ) holds
b₁ = b₂ from BINOP_2:sch 9();

func divreal -> BinOp of REAL means :: BINOP_2:def 12
for r1, r2 being Real holds it . (r1,r2) = r1 / r2;

existence
ex b₁ being BinOp of REAL st
for r1, r2 being Real holds b₁ . (r1,r2) = r1 / r2 from BINOP_2:sch 14();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Real holds b₁ . (r1,r2) = r1 / r2 ) & ( for r1, r2 being Real holds b₂ . (r1,r2) = r1 / r2 ) holds
b₁ = b₂ from BINOP_2:sch 9();

end;

:: deftheorem defines compreal BINOP_2:def 7 :
for b₁ being UnOp of REAL holds
( b₁ = compreal iff for r being Real holds b₁ . r = - r );

:: deftheorem defines invreal BINOP_2:def 8 :
for b₁ being UnOp of REAL holds
( b₁ = invreal iff for r being Real holds b₁ . r = r " );

:: deftheorem Def9 defines addreal BINOP_2:def 9 :
for b₁ being BinOp of REAL holds
( b₁ = addreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 + r2 );

:: deftheorem defines diffreal BINOP_2:def 10 :
for b₁ being BinOp of REAL holds
( b₁ = diffreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 - r2 );

:: deftheorem Def11 defines multreal BINOP_2:def 11 :
for b₁ being BinOp of REAL holds
( b₁ = multreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 * r2 );

:: deftheorem defines divreal BINOP_2:def 12 :
for b₁ being BinOp of REAL holds
( b₁ = divreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 / r2 );

definition

func comprat -> UnOp of RAT means :: BINOP_2:def 13
for w being Rational holds it . w = - w;

existence
ex b₁ being UnOp of RAT st
for w being Rational holds b₁ . w = - w from BINOP_2:sch 20();
uniqueness
for b₁, b₂ being UnOp of RAT st ( for w being Rational holds b₁ . w = - w ) & ( for w being Rational holds b₂ . w = - w ) holds
b₁ = b₂ from BINOP_2:sch 5();

func invrat -> UnOp of RAT means :: BINOP_2:def 14
for w being Rational holds it . w = w " ;

existence
ex b₁ being UnOp of RAT st
for w being Rational holds b₁ . w = w " from BINOP_2:sch 20();
uniqueness
for b₁, b₂ being UnOp of RAT st ( for w being Rational holds b₁ . w = w " ) & ( for w being Rational holds b₂ . w = w " ) holds
b₁ = b₂ from BINOP_2:sch 5();

func addrat -> BinOp of RAT means :Def15: :: BINOP_2:def 15
for w1, w2 being Rational holds it . (w1,w2) = w1 + w2;

existence
ex b₁ being BinOp of RAT st
for w1, w2 being Rational holds b₁ . (w1,w2) = w1 + w2 from BINOP_2:sch 15();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Rational holds b₁ . (w1,w2) = w1 + w2 ) & ( for w1, w2 being Rational holds b₂ . (w1,w2) = w1 + w2 ) holds
b₁ = b₂ from BINOP_2:sch 10();

func diffrat -> BinOp of RAT means :: BINOP_2:def 16
for w1, w2 being Rational holds it . (w1,w2) = w1 - w2;

existence
ex b₁ being BinOp of RAT st
for w1, w2 being Rational holds b₁ . (w1,w2) = w1 - w2 from BINOP_2:sch 15();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Rational holds b₁ . (w1,w2) = w1 - w2 ) & ( for w1, w2 being Rational holds b₂ . (w1,w2) = w1 - w2 ) holds
b₁ = b₂ from BINOP_2:sch 10();

func multrat -> BinOp of RAT means :Def17: :: BINOP_2:def 17
for w1, w2 being Rational holds it . (w1,w2) = w1 * w2;

existence
ex b₁ being BinOp of RAT st
for w1, w2 being Rational holds b₁ . (w1,w2) = w1 * w2 from BINOP_2:sch 15();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Rational holds b₁ . (w1,w2) = w1 * w2 ) & ( for w1, w2 being Rational holds b₂ . (w1,w2) = w1 * w2 ) holds
b₁ = b₂ from BINOP_2:sch 10();

func divrat -> BinOp of RAT means :: BINOP_2:def 18
for w1, w2 being Rational holds it . (w1,w2) = w1 / w2;

existence
ex b₁ being BinOp of RAT st
for w1, w2 being Rational holds b₁ . (w1,w2) = w1 / w2 from BINOP_2:sch 15();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Rational holds b₁ . (w1,w2) = w1 / w2 ) & ( for w1, w2 being Rational holds b₂ . (w1,w2) = w1 / w2 ) holds
b₁ = b₂ from BINOP_2:sch 10();

end;

:: deftheorem defines comprat BINOP_2:def 13 :
for b₁ being UnOp of RAT holds
( b₁ = comprat iff for w being Rational holds b₁ . w = - w );

:: deftheorem defines invrat BINOP_2:def 14 :
for b₁ being UnOp of RAT holds
( b₁ = invrat iff for w being Rational holds b₁ . w = w " );

:: deftheorem Def15 defines addrat BINOP_2:def 15 :
for b₁ being BinOp of RAT holds
( b₁ = addrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 + w2 );

:: deftheorem defines diffrat BINOP_2:def 16 :
for b₁ being BinOp of RAT holds
( b₁ = diffrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 - w2 );

:: deftheorem Def17 defines multrat BINOP_2:def 17 :
for b₁ being BinOp of RAT holds
( b₁ = multrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 * w2 );

:: deftheorem defines divrat BINOP_2:def 18 :
for b₁ being BinOp of RAT holds
( b₁ = divrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 / w2 );

definition

func compint -> UnOp of INT means :: BINOP_2:def 19
for i being Integer holds it . i = - i;

existence
ex b₁ being UnOp of INT st
for i being Integer holds b₁ . i = - i from BINOP_2:sch 21();
uniqueness
for b₁, b₂ being UnOp of INT st ( for i being Integer holds b₁ . i = - i ) & ( for i being Integer holds b₂ . i = - i ) holds
b₁ = b₂ from BINOP_2:sch 6();

func addint -> BinOp of INT means :Def20: :: BINOP_2:def 20
for i1, i2 being Integer holds it . (i1,i2) = i1 + i2;

existence
ex b₁ being BinOp of INT st
for i1, i2 being Integer holds b₁ . (i1,i2) = i1 + i2 from BINOP_2:sch 16();
uniqueness
for b₁, b₂ being BinOp of INT st ( for i1, i2 being Integer holds b₁ . (i1,i2) = i1 + i2 ) & ( for i1, i2 being Integer holds b₂ . (i1,i2) = i1 + i2 ) holds
b₁ = b₂ from BINOP_2:sch 11();

func diffint -> BinOp of INT means :: BINOP_2:def 21
for i1, i2 being Integer holds it . (i1,i2) = i1 - i2;

existence
ex b₁ being BinOp of INT st
for i1, i2 being Integer holds b₁ . (i1,i2) = i1 - i2 from BINOP_2:sch 16();
uniqueness
for b₁, b₂ being BinOp of INT st ( for i1, i2 being Integer holds b₁ . (i1,i2) = i1 - i2 ) & ( for i1, i2 being Integer holds b₂ . (i1,i2) = i1 - i2 ) holds
b₁ = b₂ from BINOP_2:sch 11();

func multint -> BinOp of INT means :Def22: :: BINOP_2:def 22
for i1, i2 being Integer holds it . (i1,i2) = i1 * i2;

existence
ex b₁ being BinOp of INT st
for i1, i2 being Integer holds b₁ . (i1,i2) = i1 * i2 from BINOP_2:sch 16();
uniqueness
for b₁, b₂ being BinOp of INT st ( for i1, i2 being Integer holds b₁ . (i1,i2) = i1 * i2 ) & ( for i1, i2 being Integer holds b₂ . (i1,i2) = i1 * i2 ) holds
b₁ = b₂ from BINOP_2:sch 11();

end;

:: deftheorem defines compint BINOP_2:def 19 :
for b₁ being UnOp of INT holds
( b₁ = compint iff for i being Integer holds b₁ . i = - i );

:: deftheorem Def20 defines addint BINOP_2:def 20 :
for b₁ being BinOp of INT holds
( b₁ = addint iff for i1, i2 being Integer holds b₁ . (i1,i2) = i1 + i2 );

:: deftheorem defines diffint BINOP_2:def 21 :
for b₁ being BinOp of INT holds
( b₁ = diffint iff for i1, i2 being Integer holds b₁ . (i1,i2) = i1 - i2 );

:: deftheorem Def22 defines multint BINOP_2:def 22 :
for b₁ being BinOp of INT holds
( b₁ = multint iff for i1, i2 being Integer holds b₁ . (i1,i2) = i1 * i2 );

definition

func addnat -> BinOp of NAT means :Def23: :: BINOP_2:def 23
for n1, n2 being Nat holds it . (n1,n2) = n1 + n2;

existence
ex b₁ being BinOp of NAT st
for n1, n2 being Nat holds b₁ . (n1,n2) = n1 + n2 from BINOP_2:sch 17();
uniqueness
for b₁, b₂ being BinOp of NAT st ( for n1, n2 being Nat holds b₁ . (n1,n2) = n1 + n2 ) & ( for n1, n2 being Nat holds b₂ . (n1,n2) = n1 + n2 ) holds
b₁ = b₂ from BINOP_2:sch 12();

func multnat -> BinOp of NAT means :Def24: :: BINOP_2:def 24
for n1, n2 being Nat holds it . (n1,n2) = n1 * n2;

existence
ex b₁ being BinOp of NAT st
for n1, n2 being Nat holds b₁ . (n1,n2) = n1 * n2 from BINOP_2:sch 17();
uniqueness
for b₁, b₂ being BinOp of NAT st ( for n1, n2 being Nat holds b₁ . (n1,n2) = n1 * n2 ) & ( for n1, n2 being Nat holds b₂ . (n1,n2) = n1 * n2 ) holds
b₁ = b₂ from BINOP_2:sch 12();

end;

:: deftheorem Def23 defines addnat BINOP_2:def 23 :
for b₁ being BinOp of NAT holds
( b₁ = addnat iff for n1, n2 being Nat holds b₁ . (n1,n2) = n1 + n2 );

:: deftheorem Def24 defines multnat BINOP_2:def 24 :
for b₁ being BinOp of NAT holds
( b₁ = multnat iff for n1, n2 being Nat holds b₁ . (n1,n2) = n1 * n2 );

registration

cluster addcomplex -> commutative associative ;

coherence
( addcomplex is commutative & addcomplex is associative )

proof end;

cluster multcomplex -> commutative associative ;

coherence
( multcomplex is commutative & multcomplex is associative )

proof end;

cluster addreal -> commutative associative ;

coherence
( addreal is commutative & addreal is associative )

proof end;

cluster multreal -> commutative associative ;

coherence
( multreal is commutative & multreal is associative )

proof end;

cluster addrat -> commutative associative ;

coherence
( addrat is commutative & addrat is associative )

proof end;

cluster multrat -> commutative associative ;

coherence
( multrat is commutative & multrat is associative )

proof end;

cluster addint -> commutative associative ;

coherence
( addint is commutative & addint is associative )

proof end;

cluster multint -> commutative associative ;

coherence
( multint is commutative & multint is associative )

proof end;

cluster addnat -> commutative associative ;

coherence
( addnat is commutative & addnat is associative )

proof end;

cluster multnat -> commutative associative ;

coherence
( multnat is commutative & multnat is associative )

proof end;

end;

Lm1: 0 in NAT
;

Lm2: 0 is_a_unity_wrt addcomplex

proof end;

Lm3: In (0,REAL) is_a_unity_wrt addreal

proof end;

Lm4: 0 is_a_unity_wrt addrat

proof end;

Lm5: 0 is_a_unity_wrt addint

proof end;

Lm6: 0 is_a_unity_wrt addnat

proof end;

Lm7: 1 in NAT
;

Lm8: 1 is_a_unity_wrt multcomplex

proof end;

Lm9: 1 is_a_unity_wrt multreal

proof end;

Lm10: 1 is_a_unity_wrt multrat

proof end;

Lm11: 1 is_a_unity_wrt multint

proof end;

Lm12: 1 is_a_unity_wrt multnat

proof end;

registration

cluster addcomplex -> having_a_unity ;

coherence
addcomplex is having_a_unity by Lm1, NUMBERS:20, Lm2, SETWISEO:def 2;

cluster addreal -> having_a_unity ;

coherence
addreal is having_a_unity by Lm3, SETWISEO:def 2;

cluster addrat -> having_a_unity ;

coherence
addrat is having_a_unity by Lm1, NUMBERS:18, Lm4, SETWISEO:def 2;

cluster addint -> having_a_unity ;

coherence
addint is having_a_unity by Lm1, NUMBERS:17, Lm5, SETWISEO:def 2;

cluster addnat -> having_a_unity ;

coherence
addnat is having_a_unity by Lm6, SETWISEO:def 2;

cluster multcomplex -> having_a_unity ;

coherence
multcomplex is having_a_unity by Lm7, NUMBERS:20, Lm8, SETWISEO:def 2;

cluster multreal -> having_a_unity ;

coherence
multreal is having_a_unity by Lm7, NUMBERS:19, Lm9, SETWISEO:def 2;

cluster multrat -> having_a_unity ;

coherence
multrat is having_a_unity by Lm7, NUMBERS:18, Lm10, SETWISEO:def 2;

cluster multint -> having_a_unity ;

coherence
multint is having_a_unity by Lm7, NUMBERS:17, Lm11, SETWISEO:def 2;

cluster multnat -> having_a_unity ;

coherence
multnat is having_a_unity by Lm12, SETWISEO:def 2;

end;

theorem :: BINOP_2:1

the_unity_wrt addcomplex = 0 by Lm1, NUMBERS:20, Lm2, BINOP_1:def 8;

theorem :: BINOP_2:2

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

theorem :: BINOP_2:3

the_unity_wrt addrat = 0 by Lm1, NUMBERS:18, Lm4, BINOP_1:def 8;

theorem :: BINOP_2:4

the_unity_wrt addint = 0 by Lm1, NUMBERS:17, Lm5, BINOP_1:def 8;

theorem :: BINOP_2:5

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

theorem :: BINOP_2:6

the_unity_wrt multcomplex = 1 by Lm7, NUMBERS:20, Lm8, BINOP_1:def 8;

theorem :: BINOP_2:7

the_unity_wrt multreal = 1 by Lm7, NUMBERS:19, Lm9, BINOP_1:def 8;

theorem :: BINOP_2:8

the_unity_wrt multrat = 1 by Lm7, NUMBERS:18, Lm10, BINOP_1:def 8;

theorem :: BINOP_2:9

the_unity_wrt multint = 1 by Lm7, NUMBERS:17, Lm11, BINOP_1:def 8;

theorem :: BINOP_2:10

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

registration

let f be real-valued Function;
let a, b be object ;

cluster f . (a,b) -> real ;

coherence
f . (a,b) is real ;

end;