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

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

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₁()) -> set } :

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;

registration

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

end;

definition

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

end;

definition

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

end;

definition

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

end;

definition

let i1 be Element of INT ;
:: original: -
redefine func - i1 -> Element of INT ;
coherence
- i1 is Element of INT by INT_1:def 2;
let i2 be Element of INT ;
:: original: +
redefine func i1 + i2 -> Element of INT ;
coherence
i1 + i2 is Element of INT by INT_1:def 2;
:: original: -
redefine func i1 - i2 -> Element of INT ;
coherence
i1 - i2 is Element of INT by INT_1:def 2;
:: original: *
redefine func i1 * i2 -> Element of INT ;
coherence
i1 * i2 is Element of INT by INT_1:def 2;

end;

definition

let n1, n2 be Element of NAT ;
:: original: +
redefine func n1 + n2 -> Element of NAT ;
coherence
n1 + n2 is Element of NAT by ORDINAL1:def 13;
:: original: *
redefine func n1 * n2 -> Element of NAT ;
coherence
n1 * n2 is Element of NAT by ORDINAL1:def 13;

end;

definition

func compcomplex -> UnOp of COMPLEX means :: BINOP_2:def 1
for c being Element of COMPLEX holds it . c = - c;
existence
ex b₁ being UnOp of COMPLEX st
for c being Element of COMPLEX holds b₁ . c = - c from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of COMPLEX st ( for c being Element of COMPLEX holds b₁ . c = - c ) & ( for c being Element of COMPLEX holds b₂ . c = - c ) holds
b₁ = b₂ from BINOP_2:sch 1();
func invcomplex -> UnOp of COMPLEX means :: BINOP_2:def 2
for c being Element of COMPLEX holds it . c = c " ;
existence
ex b₁ being UnOp of COMPLEX st
for c being Element of COMPLEX holds b₁ . c = c " from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of COMPLEX st ( for c being Element of COMPLEX holds b₁ . c = c " ) & ( for c being Element of COMPLEX holds b₂ . c = c " ) holds
b₁ = b₂ from BINOP_2:sch 1();
func addcomplex -> BinOp of COMPLEX means :Def3: :: BINOP_2:def 3
for c1, c2 being Element of COMPLEX holds it . c1,c2 = c1 + c2;
existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 + c2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 + c2 ) & ( for c1, c2 being Element of COMPLEX holds b₂ . c1,c2 = c1 + c2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func diffcomplex -> BinOp of COMPLEX means :: BINOP_2:def 4
for c1, c2 being Element of COMPLEX holds it . c1,c2 = c1 - c2;
existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 - c2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 - c2 ) & ( for c1, c2 being Element of COMPLEX holds b₂ . c1,c2 = c1 - c2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func multcomplex -> BinOp of COMPLEX means :Def5: :: BINOP_2:def 5
for c1, c2 being Element of COMPLEX holds it . c1,c2 = c1 * c2;
existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 * c2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 * c2 ) & ( for c1, c2 being Element of COMPLEX holds b₂ . c1,c2 = c1 * c2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func divcomplex -> BinOp of COMPLEX means :: BINOP_2:def 6
for c1, c2 being Element of COMPLEX holds it . c1,c2 = c1 / c2;
existence
ex b₁ being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 / c2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b₁ . c1,c2 = c1 / c2 ) & ( for c1, c2 being Element of COMPLEX holds b₂ . c1,c2 = c1 / c2 ) holds
b₁ = b₂ from BINOP_2:sch 2();

end;

:: deftheorem defines compcomplex BINOP_2:def 1 :

for b₁ being UnOp of COMPLEX holds
( b₁ = compcomplex iff for c being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of COMPLEX holds b₁ . c1,c2 = c1 / c2 );

definition

func compreal -> UnOp of REAL means :: BINOP_2:def 7
for r being Element of REAL holds it . r = - r;
existence
ex b₁ being UnOp of REAL st
for r being Element of REAL holds b₁ . r = - r from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of REAL st ( for r being Element of REAL holds b₁ . r = - r ) & ( for r being Element of REAL holds b₂ . r = - r ) holds
b₁ = b₂ from BINOP_2:sch 1();
func invreal -> UnOp of REAL means :: BINOP_2:def 8
for r being Element of REAL holds it . r = r " ;
existence
ex b₁ being UnOp of REAL st
for r being Element of REAL holds b₁ . r = r " from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of REAL st ( for r being Element of REAL holds b₁ . r = r " ) & ( for r being Element of REAL holds b₂ . r = r " ) holds
b₁ = b₂ from BINOP_2:sch 1();
func addreal -> BinOp of REAL means :Def9: :: BINOP_2:def 9
for r1, r2 being Element of REAL holds it . r1,r2 = r1 + r2;
existence
ex b₁ being BinOp of REAL st
for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 + r2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 + r2 ) & ( for r1, r2 being Element of REAL holds b₂ . r1,r2 = r1 + r2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func diffreal -> BinOp of REAL means :: BINOP_2:def 10
for r1, r2 being Element of REAL holds it . r1,r2 = r1 - r2;
existence
ex b₁ being BinOp of REAL st
for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 - r2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 - r2 ) & ( for r1, r2 being Element of REAL holds b₂ . r1,r2 = r1 - r2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func multreal -> BinOp of REAL means :Def11: :: BINOP_2:def 11
for r1, r2 being Element of REAL holds it . r1,r2 = r1 * r2;
existence
ex b₁ being BinOp of REAL st
for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 * r2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 * r2 ) & ( for r1, r2 being Element of REAL holds b₂ . r1,r2 = r1 * r2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func divreal -> BinOp of REAL means :: BINOP_2:def 12
for r1, r2 being Element of REAL holds it . r1,r2 = r1 / r2;
existence
ex b₁ being BinOp of REAL st
for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 / r2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of REAL st ( for r1, r2 being Element of REAL holds b₁ . r1,r2 = r1 / r2 ) & ( for r1, r2 being Element of REAL holds b₂ . r1,r2 = r1 / r2 ) holds
b₁ = b₂ from BINOP_2:sch 2();

end;

:: deftheorem defines compreal BINOP_2:def 7 :

for b₁ being UnOp of REAL holds
( b₁ = compreal iff for r being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of REAL holds b₁ . r1,r2 = r1 / r2 );

definition

func comprat -> UnOp of RAT means :: BINOP_2:def 13
for w being Element of RAT holds it . w = - w;
existence
ex b₁ being UnOp of RAT st
for w being Element of RAT holds b₁ . w = - w from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of RAT st ( for w being Element of RAT holds b₁ . w = - w ) & ( for w being Element of RAT holds b₂ . w = - w ) holds
b₁ = b₂ from BINOP_2:sch 1();
func invrat -> UnOp of RAT means :: BINOP_2:def 14
for w being Element of RAT holds it . w = w " ;
existence
ex b₁ being UnOp of RAT st
for w being Element of RAT holds b₁ . w = w " from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of RAT st ( for w being Element of RAT holds b₁ . w = w " ) & ( for w being Element of RAT holds b₂ . w = w " ) holds
b₁ = b₂ from BINOP_2:sch 1();
func addrat -> BinOp of RAT means :Def15: :: BINOP_2:def 15
for w1, w2 being Element of RAT holds it . w1,w2 = w1 + w2;
existence
ex b₁ being BinOp of RAT st
for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 + w2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 + w2 ) & ( for w1, w2 being Element of RAT holds b₂ . w1,w2 = w1 + w2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func diffrat -> BinOp of RAT means :: BINOP_2:def 16
for w1, w2 being Element of RAT holds it . w1,w2 = w1 - w2;
existence
ex b₁ being BinOp of RAT st
for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 - w2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 - w2 ) & ( for w1, w2 being Element of RAT holds b₂ . w1,w2 = w1 - w2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func multrat -> BinOp of RAT means :Def17: :: BINOP_2:def 17
for w1, w2 being Element of RAT holds it . w1,w2 = w1 * w2;
existence
ex b₁ being BinOp of RAT st
for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 * w2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 * w2 ) & ( for w1, w2 being Element of RAT holds b₂ . w1,w2 = w1 * w2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func divrat -> BinOp of RAT means :: BINOP_2:def 18
for w1, w2 being Element of RAT holds it . w1,w2 = w1 / w2;
existence
ex b₁ being BinOp of RAT st
for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 / w2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of RAT st ( for w1, w2 being Element of RAT holds b₁ . w1,w2 = w1 / w2 ) & ( for w1, w2 being Element of RAT holds b₂ . w1,w2 = w1 / w2 ) holds
b₁ = b₂ from BINOP_2:sch 2();

end;

:: deftheorem defines comprat BINOP_2:def 13 :

for b₁ being UnOp of RAT holds
( b₁ = comprat iff for w being Element of RAT holds b₁ . w = - w );

:: deftheorem defines invrat BINOP_2:def 14 :

for b₁ being UnOp of RAT holds
( b₁ = invrat iff for w being Element of RAT 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 Element of RAT 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 Element of RAT 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 Element of RAT 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 Element of RAT holds b₁ . w1,w2 = w1 / w2 );

definition

func compint -> UnOp of INT means :: BINOP_2:def 19
for i being Element of INT holds it . i = - i;
existence
ex b₁ being UnOp of INT st
for i being Element of INT holds b₁ . i = - i from FUNCT_2:sch 4();
uniqueness
for b₁, b₂ being UnOp of INT st ( for i being Element of INT holds b₁ . i = - i ) & ( for i being Element of INT holds b₂ . i = - i ) holds
b₁ = b₂ from BINOP_2:sch 1();
func addint -> BinOp of INT means :Def20: :: BINOP_2:def 20
for i1, i2 being Element of INT holds it . i1,i2 = i1 + i2;
existence
ex b₁ being BinOp of INT st
for i1, i2 being Element of INT holds b₁ . i1,i2 = i1 + i2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of INT st ( for i1, i2 being Element of INT holds b₁ . i1,i2 = i1 + i2 ) & ( for i1, i2 being Element of INT holds b₂ . i1,i2 = i1 + i2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func diffint -> BinOp of INT means :: BINOP_2:def 21
for i1, i2 being Element of INT holds it . i1,i2 = i1 - i2;
existence
ex b₁ being BinOp of INT st
for i1, i2 being Element of INT holds b₁ . i1,i2 = i1 - i2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of INT st ( for i1, i2 being Element of INT holds b₁ . i1,i2 = i1 - i2 ) & ( for i1, i2 being Element of INT holds b₂ . i1,i2 = i1 - i2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func multint -> BinOp of INT means :Def22: :: BINOP_2:def 22
for i1, i2 being Element of INT holds it . i1,i2 = i1 * i2;
existence
ex b₁ being BinOp of INT st
for i1, i2 being Element of INT holds b₁ . i1,i2 = i1 * i2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of INT st ( for i1, i2 being Element of INT holds b₁ . i1,i2 = i1 * i2 ) & ( for i1, i2 being Element of INT holds b₂ . i1,i2 = i1 * i2 ) holds
b₁ = b₂ from BINOP_2:sch 2();

end;

:: deftheorem defines compint BINOP_2:def 19 :

for b₁ being UnOp of INT holds
( b₁ = compint iff for i being Element of INT 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 Element of INT 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 Element of INT 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 Element of INT holds b₁ . i1,i2 = i1 * i2 );

definition

func addnat -> BinOp of NAT means :Def23: :: BINOP_2:def 23
for n1, n2 being Element of NAT holds it . n1,n2 = n1 + n2;
existence
ex b₁ being BinOp of NAT st
for n1, n2 being Element of NAT holds b₁ . n1,n2 = n1 + n2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of NAT st ( for n1, n2 being Element of NAT holds b₁ . n1,n2 = n1 + n2 ) & ( for n1, n2 being Element of NAT holds b₂ . n1,n2 = n1 + n2 ) holds
b₁ = b₂ from BINOP_2:sch 2();
func multnat -> BinOp of NAT means :Def24: :: BINOP_2:def 24
for n1, n2 being Element of NAT holds it . n1,n2 = n1 * n2;
existence
ex b₁ being BinOp of NAT st
for n1, n2 being Element of NAT holds b₁ . n1,n2 = n1 * n2 from BINOP_1:sch 4();
uniqueness
for b₁, b₂ being BinOp of NAT st ( for n1, n2 being Element of NAT holds b₁ . n1,n2 = n1 * n2 ) & ( for n1, n2 being Element of NAT holds b₂ . n1,n2 = n1 * n2 ) holds
b₁ = b₂ from BINOP_2:sch 2();

end;

:: deftheorem Def23 defines addnat BINOP_2:def 23 :

for b₁ being BinOp of NAT holds
( b₁ = addnat iff for n1, n2 being Element of 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 Element of 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
;

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

Lm2: z is_a_unity_wrt addcomplex

proof end;

Lm3: 0 is_a_unity_wrt addreal

proof end;

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

Lm4: z is_a_unity_wrt addrat

proof end;

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

Lm5: z is_a_unity_wrt addint

proof end;

Lm6: 0 is_a_unity_wrt addnat

proof end;

Lm7: 1 in NAT
;

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

Lm8: z is_a_unity_wrt multcomplex

proof end;

Lm9: 1 is_a_unity_wrt multreal

proof end;

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

Lm10: z is_a_unity_wrt multrat

proof end;

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

Lm11: z 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 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 Lm4, SETWISEO:def 2;
cluster addint -> having_a_unity ;
coherence
addint is having_a_unity by 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 Lm8, SETWISEO:def 2;
cluster multreal -> having_a_unity ;
coherence
multreal is having_a_unity by Lm9, SETWISEO:def 2;
cluster multrat -> having_a_unity ;
coherence
multrat is having_a_unity by Lm10, SETWISEO:def 2;
cluster multint -> having_a_unity ;
coherence
multint is having_a_unity by 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 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 Lm4, BINOP_1:def 8;

theorem :: BINOP_2:4

the_unity_wrt addint = 0 by 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 Lm8, BINOP_1:def 8;

theorem :: BINOP_2:7

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

theorem :: BINOP_2:8

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

theorem :: BINOP_2:9

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

theorem :: BINOP_2:10

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