:: 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() holds
( ( for b3 being Element of F1() holds b1 . b3 = F3(b3) ) & ( for b3 being Element of F1() holds b2 . b3 = F3(b3) ) implies b1 = b2 )
proof
let c1, c2 be Function of F1(),F2();
assume that
E1: for b1 being Element of F1() holds c1 . b1 = F3(b1) and
E2: for b1 being Element of F1() holds c2 . b1 = F3(b1) ;
now
let c3 be Element of F1();
thus c1 . c3 = F3(c3) by E1
.= c2 . c3 by E2 ;
end;
hence c1 = c2 by FUNCT_2:113;
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() holds
( ( 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) ) implies b1 = b2 )
proof
let c1, c2 be BinOp of F1();
assume that
E1: for b1, b2 being Element of F1() holds c1 . b1,b2 = F2(b1,b2) and
E2: for b1, b2 being Element of F1() holds c2 . b1,b2 = F2(b1,b2) ;
now
let c3, c4 be Element of F1();
thus c1 . c3,c4 = F2(c3,c4) by E1
.= c2 . c3,c4 by E2 ;
end;
hence c1 = c2 by BINOP_1:2;
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 ORDINAL1:def 13;
redefine func * as c1 * c2 -> Element of NAT ;
coherence
c1 * c2 is Element of NAT by ORDINAL1:def 13;
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 holds
( ( for b3 being Element of COMPLEX holds b1 . b3 = - b3 ) & ( for b3 being Element of COMPLEX holds b2 . b3 = - b3 ) implies 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 holds
( ( for b3 being Element of COMPLEX holds b1 . b3 = b3 " ) & ( for b3 being Element of COMPLEX holds b2 . b3 = b3 " ) implies 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 4();
uniqueness
for b1, b2 being BinOp of COMPLEX holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of COMPLEX holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of COMPLEX holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of COMPLEX holds
( ( 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 ) implies 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 holds
( ( for b3 being Element of REAL holds b1 . b3 = - b3 ) & ( for b3 being Element of REAL holds b2 . b3 = - b3 ) implies 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 holds
( ( for b3 being Element of REAL holds b1 . b3 = b3 " ) & ( for b3 being Element of REAL holds b2 . b3 = b3 " ) implies 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 4();
uniqueness
for b1, b2 being BinOp of REAL holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of REAL holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of REAL holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of REAL holds
( ( 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 ) implies 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 holds
( ( for b3 being Element of RAT holds b1 . b3 = - b3 ) & ( for b3 being Element of RAT holds b2 . b3 = - b3 ) implies 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 holds
( ( for b3 being Element of RAT holds b1 . b3 = b3 " ) & ( for b3 being Element of RAT holds b2 . b3 = b3 " ) implies 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 4();
uniqueness
for b1, b2 being BinOp of RAT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of RAT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of RAT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of RAT holds
( ( 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 ) implies 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 holds
( ( for b3 being Element of INT holds b1 . b3 = - b3 ) & ( for b3 being Element of INT holds b2 . b3 = - b3 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of INT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of INT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of INT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of NAT holds
( ( 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 ) implies 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 4();
uniqueness
for b1, b2 being BinOp of NAT holds
( ( 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 ) implies 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
thus addcomplex is commutative
proof
let c1 be Element of COMPLEX ; :: according to BINOP_1:def 13
let c2 be Element of COMPLEX ;
thus addcomplex . c1,c2 = c1 + c2 by Def3
.= addcomplex . c2,c1 by Def3 ;
end;
let c1 be Element of COMPLEX ; :: according to BINOP_1:def 14
let 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
( multcomplex is commutative & multcomplex is associative )
proof
thus multcomplex is commutative
proof
let c1 be Element of COMPLEX ; :: according to BINOP_1:def 13
let c2 be Element of COMPLEX ;
thus multcomplex . c1,c2 = c1 * c2 by Def5
.= multcomplex . c2,c1 by Def5 ;
end;
let c1 be Element of COMPLEX ; :: according to BINOP_1:def 14
let 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
( addreal is commutative & addreal is associative )
proof
thus addreal is commutative
proof
let c1 be Element of REAL ; :: according to BINOP_1:def 13
let c2 be Element of REAL ;
thus addreal . c1,c2 = c1 + c2 by Def9
.= addreal . c2,c1 by Def9 ;
end;
let c1 be Element of REAL ; :: according to BINOP_1:def 14
let c2, c3 be Element of REAL ;
thus addreal . c1,(addreal . c2,c3) = c1 + (addreal . c2,c3) by Def9
.= c1 + (c2 + c3) by Def9
.= (c1 + c2) + c3
.= (addreal . c1,c2) + c3 by Def9
.= addreal . (addreal . c1,c2),c3 by Def9 ;
end;
cluster multreal -> commutative associative ;
coherence
( multreal is commutative & multreal is associative )
proof
thus multreal is commutative
proof
let c1 be Element of REAL ; :: according to BINOP_1:def 13
let c2 be Element of REAL ;
thus multreal . c1,c2 = c1 * c2 by Def11
.= multreal . c2,c1 by Def11 ;
end;
let c1 be Element of REAL ; :: according to BINOP_1:def 14
let c2, c3 be Element of REAL ;
thus multreal . c1,(multreal . c2,c3) = c1 * (multreal . c2,c3) by Def11
.= c1 * (c2 * c3) by Def11
.= (c1 * c2) * c3
.= (multreal . c1,c2) * c3 by Def11
.= multreal . (multreal . c1,c2),c3 by Def11 ;
end;
cluster addrat -> commutative associative ;
coherence
( addrat is commutative & addrat is associative )
proof
thus addrat is commutative
proof
let c1 be Element of RAT ; :: according to BINOP_1:def 13
let c2 be Element of RAT ;
thus addrat . c1,c2 = c1 + c2 by Def15
.= addrat . c2,c1 by Def15 ;
end;
let c1 be Element of RAT ; :: according to BINOP_1:def 14
let c2, c3 be Element of RAT ;
thus addrat . c1,(addrat . c2,c3) = c1 + (addrat . c2,c3) by Def15
.= c1 + (c2 + c3) by Def15
.= (c1 + c2) + c3
.= (addrat . c1,c2) + c3 by Def15
.= addrat . (addrat . c1,c2),c3 by Def15 ;
end;
cluster multrat -> commutative associative ;
coherence
( multrat is commutative & multrat is associative )
proof
thus multrat is commutative
proof
let c1 be Element of RAT ; :: according to BINOP_1:def 13
let c2 be Element of RAT ;
thus multrat . c1,c2 = c1 * c2 by Def17
.= multrat . c2,c1 by Def17 ;
end;
let c1 be Element of RAT ; :: according to BINOP_1:def 14
let c2, c3 be Element of RAT ;
thus multrat . c1,(multrat . c2,c3) = c1 * (multrat . c2,c3) by Def17
.= c1 * (c2 * c3) by Def17
.= (c1 * c2) * c3
.= (multrat . c1,c2) * c3 by Def17
.= multrat . (multrat . c1,c2),c3 by Def17 ;
end;
cluster addint -> commutative associative ;
coherence
( addint is commutative & addint is associative )
proof
thus addint is commutative
proof
let c1 be Element of INT ; :: according to BINOP_1:def 13
let c2 be Element of INT ;
thus addint . c1,c2 = c1 + c2 by Def20
.= addint . c2,c1 by Def20 ;
end;
let c1 be Element of INT ; :: according to BINOP_1:def 14
let c2, c3 be Element of INT ;
thus addint . c1,(addint . c2,c3) = c1 + (addint . c2,c3) by Def20
.= c1 + (c2 + c3) by Def20
.= (c1 + c2) + c3
.= (addint . c1,c2) + c3 by Def20
.= addint . (addint . c1,c2),c3 by Def20 ;
end;
cluster multint -> commutative associative ;
coherence
( multint is commutative & multint is associative )
proof
thus multint is commutative
proof
let c1 be Element of INT ; :: according to BINOP_1:def 13
let c2 be Element of INT ;
thus multint . c1,c2 = c1 * c2 by Def22
.= multint . c2,c1 by Def22 ;
end;
let c1 be Element of INT ; :: according to BINOP_1:def 14
let c2, c3 be Element of INT ;
thus multint . c1,(multint . c2,c3) = c1 * (multint . c2,c3) by Def22
.= c1 * (c2 * c3) by Def22
.= (c1 * c2) * c3
.= (multint . c1,c2) * c3 by Def22
.= multint . (multint . c1,c2),c3 by Def22 ;
end;
cluster addnat -> commutative associative ;
coherence
( addnat is commutative & addnat is associative )
proof
thus addnat is commutative
proof
let c1 be Element of NAT ; :: according to BINOP_1:def 13
let c2 be Element of NAT ;
thus addnat . c1,c2 = c1 + c2 by Def23
.= addnat . c2,c1 by Def23 ;
end;
let c1 be Element of NAT ; :: according to BINOP_1:def 14
let c2, c3 be Element of NAT ;
thus addnat . c1,(addnat . c2,c3) = c1 + (addnat . c2,c3) by Def23
.= c1 + (c2 + c3) by Def23
.= (c1 + c2) + c3
.= (addnat . c1,c2) + c3 by Def23
.= addnat . (addnat . c1,c2),c3 by Def23 ;
end;
cluster multnat -> commutative associative ;
coherence
(