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

for b₁, b₂ being Function of F₁(),F₂() holds
( ( for b₃ being Element of F₁() holds b₁ . b₃ = F₃(b₃) & for b₃ being Element of F₁() holds b₂ . b₃ = F₃(b₃) ) implies ( b₁ = b₂ ) )

provided

proof

let c₁, c₂ be Function of F₁(),F₂();
assume that E1: for b₁ being Element of F₁() holds c₁ . b₁ = F₃(b₁)
and E2: for b₁ being Element of F₁() holds c₂ . b₁ = F₃(b₁) ;

now

let c₃ be Element of F₁();
thus c₁ . c₃ = F₃(c₃) by E1
.= c₂ . c₃ by E2 ;

end;

hence c₁ = c₂ by FUNCT_2:113;

end;

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

for b₁, b₂ being BinOp of F₁() holds
( ( for b₃, b₄ being Element of F₁() holds b₁ . b₃,b₄ = F₂(b₃,b₄) & for b₃, b₄ being Element of F₁() holds b₂ . b₃,b₄ = F₂(b₃,b₄) ) implies ( b₁ = b₂ ) )

provided

proof

let c₁, c₂ be BinOp of F₁();
assume that E1: for b₁, b₂ being Element of F₁() holds c₁ . b₁,b₂ = F₂(b₁,b₂)
and E2: for b₁, b₂ being Element of F₁() holds c₂ . b₁,b₂ = F₂(b₁,b₂) ;

now

let c₃, c₄ be Element of F₁();
thus c₁ . c₃,c₄ = F₂(c₃,c₄) by E1
.= c₂ . c₃,c₄ by E2 ;

end;

hence c₁ = c₂ by BINOP_1:2;

end;

registration

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

end;

definition

let c₁ be Element of COMPLEX ;
redefine func - as - a₁ -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;
redefine func " as a₁ " -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;
let c₂ be Element of COMPLEX ;
redefine func + as a₁ + a₂ -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;
redefine func - as a₁ - a₂ -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;
redefine func * as a₁ * a₂ -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;
redefine func / as a₁ / a₂ -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

definition

let c₁ be Element of REAL ;
redefine func - as - a₁ -> Element of REAL ;
coherence by XREAL_0:def 1;
redefine func " as a₁ " -> Element of REAL ;
coherence by XREAL_0:def 1;
let c₂ be Element of REAL ;
redefine func + as a₁ + a₂ -> Element of REAL ;
coherence by XREAL_0:def 1;
redefine func - as a₁ - a₂ -> Element of REAL ;
coherence by XREAL_0:def 1;
redefine func * as a₁ * a₂ -> Element of REAL ;
coherence by XREAL_0:def 1;
redefine func / as a₁ / a₂ -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

definition

let c₁ be Element of RAT ;
redefine func - as - a₁ -> Element of RAT ;
coherence by RAT_1:def 2;
redefine func " as a₁ " -> Element of RAT ;
coherence by RAT_1:def 2;
let c₂ be Element of RAT ;
redefine func + as a₁ + a₂ -> Element of RAT ;
coherence by RAT_1:def 2;
redefine func - as a₁ - a₂ -> Element of RAT ;
coherence by RAT_1:def 2;
redefine func * as a₁ * a₂ -> Element of RAT ;
coherence by RAT_1:def 2;
redefine func / as a₁ / a₂ -> Element of RAT ;
coherence by RAT_1:def 2;

end;

definition

let c₁ be Element of INT ;
redefine func - as - a₁ -> Element of INT ;
coherence by INT_1:def 2;
let c₂ be Element of INT ;
redefine func + as a₁ + a₂ -> Element of INT ;
coherence by INT_1:def 2;
redefine func - as a₁ - a₂ -> Element of INT ;
coherence by INT_1:def 2;
redefine func * as a₁ * a₂ -> Element of INT ;
coherence by INT_1:def 2;

end;

definition

let c₁, c₂ be Element of NAT ;
redefine func + as a₁ + a₂ -> Element of NAT ;
coherence by ORDINAL2:def 21;
redefine func * as a₁ * a₂ -> Element of NAT ;
coherence by ORDINAL2:def 21;

end;

definition

func compcomplex -> UnOp of COMPLEX means :: BINOP_2:def 1
for b₁ being Element of COMPLEX holds a₁ . b₁ = - b₁;
existence from FUNCT_2:sch 4();
uniqueness from BINOP_2:sch 1();
func invcomplex -> UnOp of COMPLEX means :: BINOP_2:def 2
for b₁ being Element of COMPLEX holds a₁ . b₁ = b₁ " ;
existence from FUNCT_2:sch 4();
uniqueness from BINOP_2:sch 1();
func addcomplex -> BinOp of COMPLEX means :E1: :: BINOP_2:def 3
for b₁, b₂ being Element of COMPLEX holds a₁ . b₁,b₂ = b₁ + b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();
func diffcomplex -> BinOp of COMPLEX means :: BINOP_2:def 4
for b₁, b₂ being Element of COMPLEX holds a₁ . b₁,b₂ = b₁ - b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();
func multcomplex -> BinOp of COMPLEX means :E2: :: BINOP_2:def 5
for b₁, b₂ being Element of COMPLEX holds a₁ . b₁,b₂ = b₁ * b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();
func divcomplex -> BinOp of COMPLEX means :: BINOP_2:def 6
for b₁, b₂ being Element of COMPLEX holds a₁ . b₁,b₂ = b₁ / b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();

end;

definition

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

end;

definition

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

end;

definition

func compint -> UnOp of INT means :: BINOP_2:def 19
for b₁ being Element of INT holds a₁ . b₁ = - b₁;
existence from FUNCT_2:sch 4();
uniqueness from BINOP_2:sch 1();
func addint -> BinOp of INT means :E7: :: BINOP_2:def 20
for b₁, b₂ being Element of INT holds a₁ . b₁,b₂ = b₁ + b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();
func diffint -> BinOp of INT means :: BINOP_2:def 21
for b₁, b₂ being Element of INT holds a₁ . b₁,b₂ = b₁ - b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();
func multint -> BinOp of INT means :E8: :: BINOP_2:def 22
for b₁, b₂ being Element of INT holds a₁ . b₁,b₂ = b₁ * b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();

end;

definition

func addnat -> BinOp of NAT means :E9: :: BINOP_2:def 23
for b₁, b₂ being Element of NAT holds a₁ . b₁,b₂ = b₁ + b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();
func multnat -> BinOp of NAT means :E10: :: BINOP_2:def 24
for b₁, b₂ being Element of NAT holds a₁ . b₁,b₂ = b₁ * b₂;
existence from BINOP_1:sch 2();
uniqueness from BINOP_2:sch 2();

end;

registration

cluster addcomplex -> commutative associative ;
coherence

proof

thus addcomplex is commutative

proof

let c₁ be Element of COMPLEX ; :: uses BINOP_1:def 13
let c₂ be Element of COMPLEX ;
thus addcomplex . c₁,c₂ = c₁ + c₂ by E1
.= addcomplex . c₂,c₁ by E1 ;

end;

let c₁ be Element of COMPLEX ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of COMPLEX ;
thus addcomplex . c₁,(addcomplex . c₂,c₃) = c₁ + (addcomplex . c₂,c₃) by E1
.= c₁ + (c₂ + c₃) by E1
.= (c₁ + c₂) + c₃
.= (addcomplex . c₁,c₂) + c₃ by E1
.= addcomplex . (addcomplex . c₁,c₂),c₃ by E1 ;

end;

cluster multcomplex -> commutative associative ;
coherence

proof

thus multcomplex is commutative

proof

let c₁ be Element of COMPLEX ; :: uses BINOP_1:def 13
let c₂ be Element of COMPLEX ;
thus multcomplex . c₁,c₂ = c₁ * c₂ by E2
.= multcomplex . c₂,c₁ by E2 ;

end;

let c₁ be Element of COMPLEX ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of COMPLEX ;
thus multcomplex . c₁,(multcomplex . c₂,c₃) = c₁ * (multcomplex . c₂,c₃) by E2
.= c₁ * (c₂ * c₃) by E2
.= (c₁ * c₂) * c₃
.= (multcomplex . c₁,c₂) * c₃ by E2
.= multcomplex . (multcomplex . c₁,c₂),c₃ by E2 ;

end;

cluster addreal -> commutative associative ;
coherence

proof

thus addreal is commutative

proof

let c₁ be Element of REAL ; :: uses BINOP_1:def 13
let c₂ be Element of REAL ;
thus addreal . c₁,c₂ = c₁ + c₂ by E3
.= addreal . c₂,c₁ by E3 ;

end;

let c₁ be Element of REAL ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of REAL ;
thus addreal . c₁,(addreal . c₂,c₃) = c₁ + (addreal . c₂,c₃) by E3
.= c₁ + (c₂ + c₃) by E3
.= (c₁ + c₂) + c₃
.= (addreal . c₁,c₂) + c₃ by E3
.= addreal . (addreal . c₁,c₂),c₃ by E3 ;

end;

cluster multreal -> commutative associative ;
coherence

proof

thus multreal is commutative

proof

let c₁ be Element of REAL ; :: uses BINOP_1:def 13
let c₂ be Element of REAL ;
thus multreal . c₁,c₂ = c₁ * c₂ by E4
.= multreal . c₂,c₁ by E4 ;

end;

let c₁ be Element of REAL ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of REAL ;
thus multreal . c₁,(multreal . c₂,c₃) = c₁ * (multreal . c₂,c₃) by E4
.= c₁ * (c₂ * c₃) by E4
.= (c₁ * c₂) * c₃
.= (multreal . c₁,c₂) * c₃ by E4
.= multreal . (multreal . c₁,c₂),c₃ by E4 ;

end;

cluster addrat -> commutative associative ;
coherence

proof

thus addrat is commutative

proof

let c₁ be Element of RAT ; :: uses BINOP_1:def 13
let c₂ be Element of RAT ;
thus addrat . c₁,c₂ = c₁ + c₂ by E5
.= addrat . c₂,c₁ by E5 ;

end;

let c₁ be Element of RAT ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of RAT ;
thus addrat . c₁,(addrat . c₂,c₃) = c₁ + (addrat . c₂,c₃) by E5
.= c₁ + (c₂ + c₃) by E5
.= (c₁ + c₂) + c₃
.= (addrat . c₁,c₂) + c₃ by E5
.= addrat . (addrat . c₁,c₂),c₃ by E5 ;

end;

cluster multrat -> commutative associative ;
coherence

proof

thus multrat is commutative

proof

let c₁ be Element of RAT ; :: uses BINOP_1:def 13
let c₂ be Element of RAT ;
thus multrat . c₁,c₂ = c₁ * c₂ by E6
.= multrat . c₂,c₁ by E6 ;

end;

let c₁ be Element of RAT ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of RAT ;
thus multrat . c₁,(multrat . c₂,c₃) = c₁ * (multrat . c₂,c₃) by E6
.= c₁ * (c₂ * c₃) by E6
.= (c₁ * c₂) * c₃
.= (multrat . c₁,c₂) * c₃ by E6
.= multrat . (multrat . c₁,c₂),c₃ by E6 ;

end;

cluster addint -> commutative associative ;
coherence

proof

thus addint is commutative

proof

let c₁ be Element of INT ; :: uses BINOP_1:def 13
let c₂ be Element of INT ;
thus addint . c₁,c₂ = c₁ + c₂ by E7
.= addint . c₂,c₁ by E7 ;

end;

let c₁ be Element of INT ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of INT ;
thus addint . c₁,(addint . c₂,c₃) = c₁ + (addint . c₂,c₃) by E7
.= c₁ + (c₂ + c₃) by E7
.= (c₁ + c₂) + c₃
.= (addint . c₁,c₂) + c₃ by E7
.= addint . (addint . c₁,c₂),c₃ by E7 ;

end;

cluster multint -> commutative associative ;
coherence

proof

thus multint is commutative

proof

let c₁ be Element of INT ; :: uses BINOP_1:def 13
let c₂ be Element of INT ;
thus multint . c₁,c₂ = c₁ * c₂ by E8
.= multint . c₂,c₁ by E8 ;

end;

let c₁ be Element of INT ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of INT ;
thus multint . c₁,(multint . c₂,c₃) = c₁ * (multint . c₂,c₃) by E8
.= c₁ * (c₂ * c₃) by E8
.= (c₁ * c₂) * c₃
.= (multint . c₁,c₂) * c₃ by E8
.= multint . (multint . c₁,c₂),c₃ by E8 ;

end;

cluster addnat -> commutative associative ;
coherence

proof

thus addnat is commutative

proof

let c₁ be Element of NAT ; :: uses BINOP_1:def 13
let c₂ be Element of NAT ;
thus addnat . c₁,c₂ = c₁ + c₂ by E9
.= addnat . c₂,c₁ by E9 ;

end;

let c₁ be Element of NAT ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of NAT ;
thus addnat . c₁,(addnat . c₂,c₃) = c₁ + (addnat . c₂,c₃) by E9
.= c₁ + (c₂ + c₃) by E9
.= (c₁ + c₂) + c₃
.= (addnat . c₁,c₂) + c₃ by E9
.= addnat . (addnat . c₁,c₂),c₃ by E9 ;

end;

cluster multnat -> commutative associative ;
coherence

proof

thus multnat is commutative

proof

let c₁ be Element of NAT ; :: uses BINOP_1:def 13
let c₂ be Element of NAT ;
thus multnat . c₁,c₂ = c₁ * c₂ by E10
.= multnat . c₂,c₁ by E10 ;

end;

let c₁ be Element of NAT ; :: uses BINOP_1:def 14
let c₂, c₃ be Element of NAT ;
thus multnat . c₁,(multnat . c₂,c₃) = c₁ * (multnat . c₂,c₃) by E10
.= c₁ * (c₂ * c₃) by E10
.= (c₁ * c₂) * c₃
.= (multnat . c₁,c₂) * c₃ by E10
.= multnat . (multnat . c₁,c₂),c₃ by E10 ;

end;

proof

thus for b₁ being Element of COMPLEX holds addcomplex . c₁,b₁ = b₁ :: uses BINOP_1:def 7,BINOP_1:def 16

proof

let c₂ be Element of COMPLEX ;
thus addcomplex . c₁,c₂ = 0 + c₂ by E1
.= c₂ ;

end;

let c₂ be Element of COMPLEX ; :: uses BINOP_1:def 17
thus addcomplex . c₂,c₁ = c₂ + 0 by E1
.= c₂ ;

end;

proof

thus for b₁ being Element of REAL holds addreal . 0,b₁ = b₁ :: uses BINOP_1:def 7,BINOP_1:def 16

proof

let c₂ be Element of REAL ;
thus addreal . 0,c₂ = 0 + c₂ by E3
.= c₂ ;

end;

let c₂ be Element of REAL ; :: uses BINOP_1:def 17
thus addreal . c₂,0 = c₂ + 0 by E3
.= c₂ ;

end;

proof

thus for b₁ being Element of RAT holds addrat . c₂,b₁ = b₁ :: uses BINOP_1:def 7,BINOP_1:def 16

proof

let c