:: BINOP_2 semantic presentation

scheme :: BINOP_2:sch 1
s1{ F1() -> non empty set , F2() -> non empty set , F3( Element of F1()) -> set } :
for b1, b2 being Function of F1(),F2() st ( for b3 being Element of F1() holds b1 . b3 = F3(b3) ) & ( for b3 being Element of F1() holds b2 . b3 = F3(b3) ) holds
b1 = b2
proof end;

scheme :: BINOP_2:sch 2
s2{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> set } :
for b1, b2 being BinOp of F1() st ( for b3, b4 being Element of F1() holds b1 . b3,b4 = F2(b3,b4) ) & ( for b3, b4 being Element of F1() holds b2 . b3,b4 = F2(b3,b4) ) holds
b1 = b2
proof end;

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

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

definition
let c1 be Element of REAL ;
redefine func - as - c1 -> Element of REAL ;
coherence
- c1 is Element of REAL by XREAL_0:def 1;
redefine func " as c1 " -> Element of REAL ;
coherence
c1 " is Element of REAL by XREAL_0:def 1;
let c2 be Element of REAL ;
redefine func + as c1 + c2 -> Element of REAL ;
coherence
c1 + c2 is Element of REAL by XREAL_0:def 1;
redefine func - as c1 - c2 -> Element of REAL ;
coherence
c1 - c2 is Element of REAL by XREAL_0:def 1;
redefine func * as c1 * c2 -> Element of REAL ;
coherence
c1 * c2 is Element of REAL by XREAL_0:def 1;
redefine func / as c1 / c2 -> Element of REAL ;
coherence
c1 / c2 is Element of REAL by XREAL_0:def 1;
end;

definition
let c1 be Element of RAT ;
redefine func - as - c1 -> Element of RAT ;
coherence
- c1 is Element of RAT by RAT_1:def 2;
redefine func " as c1 " -> Element of RAT ;
coherence
c1 " is Element of RAT by RAT_1:def 2;
let c2 be Element of RAT ;
redefine func + as c1 + c2 -> Element of RAT ;
coherence
c1 + c2 is Element of RAT by RAT_1:def 2;
redefine func - as c1 - c2 -> Element of RAT ;
coherence
c1 - c2 is Element of RAT by RAT_1:def 2;
redefine func * as c1 * c2 -> Element of RAT ;
coherence
c1 * c2 is Element of RAT by RAT_1:def 2;
redefine func / as c1 / c2 -> Element of RAT ;
coherence
c1 / c2 is Element of RAT by RAT_1:def 2;
end;

definition
let c1 be Element of INT ;
redefine func - as - c1 -> Element of INT ;
coherence
- c1 is Element of INT by INT_1:def 2;
let c2 be Element of INT ;
redefine func + as c1 + c2 -> Element of INT ;
coherence
c1 + c2 is Element of INT by INT_1:def 2;
redefine func - as c1 - c2 -> Element of INT ;
coherence
c1 - c2 is Element of INT by INT_1:def 2;
redefine func * as c1 * c2 -> Element of INT ;
coherence
c1 * c2 is Element of INT by INT_1:def 2;
end;

definition
let c1, c2 be Element of NAT ;
redefine func + as c1 + c2 -> Element of NAT ;
coherence
c1 + c2 is Element of NAT by ORDINAL2:def 21;
redefine func * as c1 * c2 -> Element of NAT ;
coherence
c1 * c2 is Element of NAT by ORDINAL2:def 21;
end;

definition
func compcomplex -> UnOp of COMPLEX means :: BINOP_2:def 1
for b1 being Element of COMPLEX holds a1 . b1 = - b1;
existence
ex b1 being UnOp of COMPLEX st
for b2 being Element of COMPLEX holds b1 . b2 = - b2 from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of COMPLEX st ( for b3 being Element of COMPLEX holds b1 . b3 = - b3 ) & ( for b3 being Element of COMPLEX holds b2 . b3 = - b3 ) holds
b1 = b2 from BINOP_2:sch 1();
func invcomplex -> UnOp of COMPLEX means :: BINOP_2:def 2
for b1 being Element of COMPLEX holds a1 . b1 = b1 " ;
existence
ex b1 being UnOp of COMPLEX st
for b2 being Element of COMPLEX holds b1 . b2 = b2 " from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of COMPLEX st ( for b3 being Element of COMPLEX holds b1 . b3 = b3 " ) & ( for b3 being Element of COMPLEX holds b2 . b3 = b3 " ) holds
b1 = b2 from BINOP_2:sch 1();
func addcomplex -> BinOp of COMPLEX means :Def3: :: BINOP_2:def 3
for b1, b2 being Element of COMPLEX holds a1 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of COMPLEX st
for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 + b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for b3, b4 being Element of COMPLEX holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of COMPLEX holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func diffcomplex -> BinOp of COMPLEX means :: BINOP_2:def 4
for b1, b2 being Element of COMPLEX holds a1 . b1,b2 = b1 - b2;
existence
ex b1 being BinOp of COMPLEX st
for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 - b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for b3, b4 being Element of COMPLEX holds b1 . b3,b4 = b3 - b4 ) & ( for b3, b4 being Element of COMPLEX holds b2 . b3,b4 = b3 - b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func multcomplex -> BinOp of COMPLEX means :Def5: :: BINOP_2:def 5
for b1, b2 being Element of COMPLEX holds a1 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of COMPLEX st
for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 * b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for b3, b4 being Element of COMPLEX holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of COMPLEX holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func divcomplex -> BinOp of COMPLEX means :: BINOP_2:def 6
for b1, b2 being Element of COMPLEX holds a1 . b1,b2 = b1 / b2;
existence
ex b1 being BinOp of COMPLEX st
for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 / b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for b3, b4 being Element of COMPLEX holds b1 . b3,b4 = b3 / b4 ) & ( for b3, b4 being Element of COMPLEX holds b2 . b3,b4 = b3 / b4 ) holds
b1 = b2 from BINOP_2:sch 2();
end;

:: deftheorem Def1 defines compcomplex BINOP_2:def 1 :
for b1 being UnOp of COMPLEX holds
( b1 = compcomplex iff for b2 being Element of COMPLEX holds b1 . b2 = - b2 );

:: deftheorem Def2 defines invcomplex BINOP_2:def 2 :
for b1 being UnOp of COMPLEX holds
( b1 = invcomplex iff for b2 being Element of COMPLEX holds b1 . b2 = b2 " );

:: deftheorem Def3 defines addcomplex BINOP_2:def 3 :
for b1 being BinOp of COMPLEX holds
( b1 = addcomplex iff for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 + b3 );

:: deftheorem Def4 defines diffcomplex BINOP_2:def 4 :
for b1 being BinOp of COMPLEX holds
( b1 = diffcomplex iff for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 - b3 );

:: deftheorem Def5 defines multcomplex BINOP_2:def 5 :
for b1 being BinOp of COMPLEX holds
( b1 = multcomplex iff for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 * b3 );

:: deftheorem Def6 defines divcomplex BINOP_2:def 6 :
for b1 being BinOp of COMPLEX holds
( b1 = divcomplex iff for b2, b3 being Element of COMPLEX holds b1 . b2,b3 = b2 / b3 );

definition
func compreal -> UnOp of REAL means :: BINOP_2:def 7
for b1 being Element of REAL holds a1 . b1 = - b1;
existence
ex b1 being UnOp of REAL st
for b2 being Element of REAL holds b1 . b2 = - b2 from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of REAL st ( for b3 being Element of REAL holds b1 . b3 = - b3 ) & ( for b3 being Element of REAL holds b2 . b3 = - b3 ) holds
b1 = b2 from BINOP_2:sch 1();
func invreal -> UnOp of REAL means :: BINOP_2:def 8
for b1 being Element of REAL holds a1 . b1 = b1 " ;
existence
ex b1 being UnOp of REAL st
for b2 being Element of REAL holds b1 . b2 = b2 " from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of REAL st ( for b3 being Element of REAL holds b1 . b3 = b3 " ) & ( for b3 being Element of REAL holds b2 . b3 = b3 " ) holds
b1 = b2 from BINOP_2:sch 1();
func addreal -> BinOp of REAL means :Def9: :: BINOP_2:def 9
for b1, b2 being Element of REAL holds a1 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of REAL st
for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 + b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of REAL st ( for b3, b4 being Element of REAL holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of REAL holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func diffreal -> BinOp of REAL means :: BINOP_2:def 10
for b1, b2 being Element of REAL holds a1 . b1,b2 = b1 - b2;
existence
ex b1 being BinOp of REAL st
for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 - b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of REAL st ( for b3, b4 being Element of REAL holds b1 . b3,b4 = b3 - b4 ) & ( for b3, b4 being Element of REAL holds b2 . b3,b4 = b3 - b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func multreal -> BinOp of REAL means :Def11: :: BINOP_2:def 11
for b1, b2 being Element of REAL holds a1 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of REAL st
for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 * b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of REAL st ( for b3, b4 being Element of REAL holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of REAL holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func divreal -> BinOp of REAL means :: BINOP_2:def 12
for b1, b2 being Element of REAL holds a1 . b1,b2 = b1 / b2;
existence
ex b1 being BinOp of REAL st
for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 / b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of REAL st ( for b3, b4 being Element of REAL holds b1 . b3,b4 = b3 / b4 ) & ( for b3, b4 being Element of REAL holds b2 . b3,b4 = b3 / b4 ) holds
b1 = b2 from BINOP_2:sch 2();
end;

:: deftheorem Def7 defines compreal BINOP_2:def 7 :
for b1 being UnOp of REAL holds
( b1 = compreal iff for b2 being Element of REAL holds b1 . b2 = - b2 );

:: deftheorem Def8 defines invreal BINOP_2:def 8 :
for b1 being UnOp of REAL holds
( b1 = invreal iff for b2 being Element of REAL holds b1 . b2 = b2 " );

:: deftheorem Def9 defines addreal BINOP_2:def 9 :
for b1 being BinOp of REAL holds
( b1 = addreal iff for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 + b3 );

:: deftheorem Def10 defines diffreal BINOP_2:def 10 :
for b1 being BinOp of REAL holds
( b1 = diffreal iff for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 - b3 );

:: deftheorem Def11 defines multreal BINOP_2:def 11 :
for b1 being BinOp of REAL holds
( b1 = multreal iff for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 * b3 );

:: deftheorem Def12 defines divreal BINOP_2:def 12 :
for b1 being BinOp of REAL holds
( b1 = divreal iff for b2, b3 being Element of REAL holds b1 . b2,b3 = b2 / b3 );

definition
func comprat -> UnOp of RAT means :: BINOP_2:def 13
for b1 being Element of RAT holds a1 . b1 = - b1;
existence
ex b1 being UnOp of RAT st
for b2 being Element of RAT holds b1 . b2 = - b2 from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of RAT st ( for b3 being Element of RAT holds b1 . b3 = - b3 ) & ( for b3 being Element of RAT holds b2 . b3 = - b3 ) holds
b1 = b2 from BINOP_2:sch 1();
func invrat -> UnOp of RAT means :: BINOP_2:def 14
for b1 being Element of RAT holds a1 . b1 = b1 " ;
existence
ex b1 being UnOp of RAT st
for b2 being Element of RAT holds b1 . b2 = b2 " from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of RAT st ( for b3 being Element of RAT holds b1 . b3 = b3 " ) & ( for b3 being Element of RAT holds b2 . b3 = b3 " ) holds
b1 = b2 from BINOP_2:sch 1();
func addrat -> BinOp of RAT means :Def15: :: BINOP_2:def 15
for b1, b2 being Element of RAT holds a1 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of RAT st
for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 + b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of RAT st ( for b3, b4 being Element of RAT holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of RAT holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func diffrat -> BinOp of RAT means :: BINOP_2:def 16
for b1, b2 being Element of RAT holds a1 . b1,b2 = b1 - b2;
existence
ex b1 being BinOp of RAT st
for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 - b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of RAT st ( for b3, b4 being Element of RAT holds b1 . b3,b4 = b3 - b4 ) & ( for b3, b4 being Element of RAT holds b2 . b3,b4 = b3 - b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func multrat -> BinOp of RAT means :Def17: :: BINOP_2:def 17
for b1, b2 being Element of RAT holds a1 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of RAT st
for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 * b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of RAT st ( for b3, b4 being Element of RAT holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of RAT holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func divrat -> BinOp of RAT means :: BINOP_2:def 18
for b1, b2 being Element of RAT holds a1 . b1,b2 = b1 / b2;
existence
ex b1 being BinOp of RAT st
for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 / b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of RAT st ( for b3, b4 being Element of RAT holds b1 . b3,b4 = b3 / b4 ) & ( for b3, b4 being Element of RAT holds b2 . b3,b4 = b3 / b4 ) holds
b1 = b2 from BINOP_2:sch 2();
end;

:: deftheorem Def13 defines comprat BINOP_2:def 13 :
for b1 being UnOp of RAT holds
( b1 = comprat iff for b2 being Element of RAT holds b1 . b2 = - b2 );

:: deftheorem Def14 defines invrat BINOP_2:def 14 :
for b1 being UnOp of RAT holds
( b1 = invrat iff for b2 being Element of RAT holds b1 . b2 = b2 " );

:: deftheorem Def15 defines addrat BINOP_2:def 15 :
for b1 being BinOp of RAT holds
( b1 = addrat iff for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 + b3 );

:: deftheorem Def16 defines diffrat BINOP_2:def 16 :
for b1 being BinOp of RAT holds
( b1 = diffrat iff for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 - b3 );

:: deftheorem Def17 defines multrat BINOP_2:def 17 :
for b1 being BinOp of RAT holds
( b1 = multrat iff for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 * b3 );

:: deftheorem Def18 defines divrat BINOP_2:def 18 :
for b1 being BinOp of RAT holds
( b1 = divrat iff for b2, b3 being Element of RAT holds b1 . b2,b3 = b2 / b3 );

definition
func compint -> UnOp of INT means :: BINOP_2:def 19
for b1 being Element of INT holds a1 . b1 = - b1;
existence
ex b1 being UnOp of INT st
for b2 being Element of INT holds b1 . b2 = - b2 from FUNCT_2:sch 4();
uniqueness
for b1, b2 being UnOp of INT st ( for b3 being Element of INT holds b1 . b3 = - b3 ) & ( for b3 being Element of INT holds b2 . b3 = - b3 ) holds
b1 = b2 from BINOP_2:sch 1();
func addint -> BinOp of INT means :Def20: :: BINOP_2:def 20
for b1, b2 being Element of INT holds a1 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of INT st
for b2, b3 being Element of INT holds b1 . b2,b3 = b2 + b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of INT st ( for b3, b4 being Element of INT holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of INT holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func diffint -> BinOp of INT means :: BINOP_2:def 21
for b1, b2 being Element of INT holds a1 . b1,b2 = b1 - b2;
existence
ex b1 being BinOp of INT st
for b2, b3 being Element of INT holds b1 . b2,b3 = b2 - b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of INT st ( for b3, b4 being Element of INT holds b1 . b3,b4 = b3 - b4 ) & ( for b3, b4 being Element of INT holds b2 . b3,b4 = b3 - b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func multint -> BinOp of INT means :Def22: :: BINOP_2:def 22
for b1, b2 being Element of INT holds a1 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of INT st
for b2, b3 being Element of INT holds b1 . b2,b3 = b2 * b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of INT st ( for b3, b4 being Element of INT holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of INT holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2 from BINOP_2:sch 2();
end;

:: deftheorem Def19 defines compint BINOP_2:def 19 :
for b1 being UnOp of INT holds
( b1 = compint iff for b2 being Element of INT holds b1 . b2 = - b2 );

:: deftheorem Def20 defines addint BINOP_2:def 20 :
for b1 being BinOp of INT holds
( b1 = addint iff for b2, b3 being Element of INT holds b1 . b2,b3 = b2 + b3 );

:: deftheorem Def21 defines diffint BINOP_2:def 21 :
for b1 being BinOp of INT holds
( b1 = diffint iff for b2, b3 being Element of INT holds b1 . b2,b3 = b2 - b3 );

:: deftheorem Def22 defines multint BINOP_2:def 22 :
for b1 being BinOp of INT holds
( b1 = multint iff for b2, b3 being Element of INT holds b1 . b2,b3 = b2 * b3 );

definition
func addnat -> BinOp of NAT means :Def23: :: BINOP_2:def 23
for b1, b2 being Element of NAT holds a1 . b1,b2 = b1 + b2;
existence
ex b1 being BinOp of NAT st
for b2, b3 being Element of NAT holds b1 . b2,b3 = b2 + b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of NAT st ( for b3, b4 being Element of NAT holds b1 . b3,b4 = b3 + b4 ) & ( for b3, b4 being Element of NAT holds b2 . b3,b4 = b3 + b4 ) holds
b1 = b2 from BINOP_2:sch 2();
func multnat -> BinOp of NAT means :Def24: :: BINOP_2:def 24
for b1, b2 being Element of NAT holds a1 . b1,b2 = b1 * b2;
existence
ex b1 being BinOp of NAT st
for b2, b3 being Element of NAT holds b1 . b2,b3 = b2 * b3 from BINOP_1:sch 2();
uniqueness
for b1, b2 being BinOp of NAT st ( for b3, b4 being Element of NAT holds b1 . b3,b4 = b3 * b4 ) & ( for b3, b4 being Element of NAT holds b2 . b3,b4 = b3 * b4 ) holds
b1 = b2 from BINOP_2:sch 2();
end;

:: deftheorem Def23 defines addnat BINOP_2:def 23 :
for b1 being BinOp of NAT holds
( b1 = addnat iff for b2, b3 being Element of NAT holds b1 . b2,b3 = b2 + b3 );

:: deftheorem Def24 defines multnat BINOP_2:def 24 :
for b1 being BinOp of NAT holds
( b1 = multnat iff for b2, b3 being Element of NAT holds b1 . b2,b3 = b2 * b3 );

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;

Lemma11: 0 in NAT
;

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

Lemma12: c1 is_a_unity_wrt addcomplex
proof end;

Lemma13: 0 is_a_unity_wrt addreal
proof end;

reconsider c2 = 0 as Element of RAT by Lemma11, NUMBERS:18;

Lemma14: c2 is_a_unity_wrt addrat
proof end;

reconsider c3 = 0 as Element of INT by Lemma11, NUMBERS:17;

Lemma15: c3 is_a_unity_wrt addint
proof end;

Lemma16: 0 is_a_unity_wrt addnat
proof end;

Lemma17: 1 in NAT
;

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

Lemma18: c4 is_a_unity_wrt multcomplex
proof end;

Lemma19: 1 is_a_unity_wrt multreal
proof end;

reconsider c5 = 1 as Element of RAT by Lemma17, NUMBERS:18;

Lemma20: c5 is_a_unity_wrt multrat
proof end;

reconsider c6 = 1 as Element of INT by Lemma17, NUMBERS:17;

Lemma21: c6 is_a_unity_wrt multint
proof end;

Lemma22: 1 is_a_unity_wrt multnat
proof end;

registration
cluster addcomplex -> commutative associative having_a_unity ;
coherence
addcomplex is having_a_unity by Lemma12, SETWISEO:def 2;
cluster addreal -> commutative associative having_a_unity ;
coherence
addreal is having_a_unity by Lemma13, SETWISEO:def 2;
cluster addrat -> commutative associative having_a_unity ;
coherence
addrat is having_a_unity by Lemma14, SETWISEO:def 2;
cluster addint -> commutative associative having_a_unity ;
coherence
addint is having_a_unity by Lemma15, SETWISEO:def 2;
cluster addnat -> commutative associative having_a_unity ;
coherence
addnat is having_a_unity by Lemma16, SETWISEO:def 2;
cluster multcomplex -> commutative associative having_a_unity ;
coherence
multcomplex is having_a_unity by Lemma18, SETWISEO:def 2;
cluster multreal -> commutative associative having_a_unity ;
coherence
multreal is having_a_unity by Lemma19, SETWISEO:def 2;
cluster multrat -> commutative associative having_a_unity ;
coherence
multrat is having_a_unity by Lemma20, SETWISEO:def 2;
cluster multint -> commutative associative having_a_unity ;
coherence
multint is having_a_unity by Lemma21, SETWISEO:def 2;
cluster multnat -> commutative associative having_a_unity ;
coherence
multnat is having_a_unity by Lemma22, SETWISEO:def 2;
end;

theorem Th1: :: BINOP_2:1
the_unity_wrt addcomplex = 0 by Lemma12, BINOP_1:def 8;

theorem Th2: :: BINOP_2:2
the_unity_wrt addreal = 0 by Lemma13, BINOP_1:def 8;

theorem Th3: :: BINOP_2:3
the_unity_wrt addrat = 0 by Lemma14, BINOP_1:def 8;

theorem Th4: :: BINOP_2:4
the_unity_wrt addint = 0 by Lemma15, BINOP_1:def 8;

theorem Th5: :: BINOP_2:5
the_unity_wrt addnat = 0 by Lemma16, BINOP_1:def 8;

theorem Th6: :: BINOP_2:6
the_unity_wrt multcomplex = 1 by Lemma18, BINOP_1:def 8;

theorem Th7: :: BINOP_2:7
the_unity_wrt multreal = 1 by Lemma19, BINOP_1:def 8;

theorem Th8: :: BINOP_2:8
the_unity_wrt multrat = 1 by Lemma20, BINOP_1:def 8;

theorem Th9: :: BINOP_2:9
the_unity_wrt multint = 1 by Lemma21, BINOP_1:def 8;

theorem Th10: :: BINOP_2:10
the_unity_wrt multnat = 1 by Lemma22, BINOP_1:def 8;