:: BINOP_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: BINOP_2:sch 1
FuncDefUniq{ F1() -> non empty set , F2() -> non empty set , F3( Element of F1()) -> set } :
for f1, f2 being Function of F1(),F2() st ( for x being Element of F1() holds f1 . x = F3(x) ) & ( for x being Element of F1() holds f2 . x = F3(x) ) holds
f1 = f2
proof end;

scheme :: BINOP_2:sch 2
BinOpDefuniq{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> set } :
for o1, o2 being BinOp of F1() st ( for a, b being Element of F1() holds o1 . a,b = F2(a,b) ) & ( for a, b being Element of F1() holds o2 . a,b = F2(a,b) ) holds
o1 = o2
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 ;
:: 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 ORDINAL2:def 21;
:: original: *
redefine func n1 * n2 -> Element of NAT ;
coherence
n1 * n2 is Element of NAT by ORDINAL2:def 21;
end;

definition
func compcomplex -> UnOp of COMPLEX means :: BINOP_2:def 1
for c being Element of COMPLEX holds it . c = - c;
existence
ex b1 being UnOp of COMPLEX st
for c being Element of COMPLEX holds b1 . c = - c from FUNCT_2:sch 4( COMPLEX COMPLEX );
uniqueness
for b1, b2 being UnOp of COMPLEX st ( for c being Element of COMPLEX holds b1 . c = - c ) & ( for c being Element of COMPLEX holds b2 . c = - c ) holds
b1 = b2 from BINOP_2:sch 1( COMPLEX COMPLEX );
func invcomplex -> UnOp of COMPLEX means :: BINOP_2:def 2
for c being Element of COMPLEX holds it . c = c " ;
existence
ex b1 being UnOp of COMPLEX st
for c being Element of COMPLEX holds b1 . c = c " from FUNCT_2:sch 4( COMPLEX COMPLEX );
uniqueness
for b1, b2 being UnOp of COMPLEX st ( for c being Element of COMPLEX holds b1 . c = c " ) & ( for c being Element of COMPLEX holds b2 . c = c " ) holds
b1 = b2 from BINOP_2:sch 1( COMPLEX COMPLEX );
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 b1 being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 + c2 from BINOP_1:sch 2( COMPLEX );
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 + c2 ) & ( for c1, c2 being Element of COMPLEX holds b2 . c1,c2 = c1 + c2 ) holds
b1 = b2 from BINOP_2:sch 2( COMPLEX );
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 b1 being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 - c2 from BINOP_1:sch 2( COMPLEX );
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 - c2 ) & ( for c1, c2 being Element of COMPLEX holds b2 . c1,c2 = c1 - c2 ) holds
b1 = b2 from BINOP_2:sch 2( COMPLEX );
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 b1 being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 * c2 from BINOP_1:sch 2( COMPLEX );
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 * c2 ) & ( for c1, c2 being Element of COMPLEX holds b2 . c1,c2 = c1 * c2 ) holds
b1 = b2 from BINOP_2:sch 2( COMPLEX );
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 b1 being BinOp of COMPLEX st
for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 / c2 from BINOP_1:sch 2( COMPLEX );
uniqueness
for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being Element of COMPLEX holds b1 . c1,c2 = c1 / c2 ) & ( for c1, c2 being Element of COMPLEX holds b2 . c1,c2 = c1 / c2 ) holds
b1 = b2 from BINOP_2:sch 2( COMPLEX );
end;

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

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

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

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

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

:: deftheorem defines divcomplex BINOP_2:def 6 :
for b1 being BinOp of COMPLEX holds
( b1 = divcomplex iff for c1, c2 being Element of COMPLEX holds b1 . 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 b1 being UnOp of REAL st
for r being Element of REAL holds b1 . r = - r from FUNCT_2:sch 4( REAL REAL );
uniqueness
for b1, b2 being UnOp of REAL st ( for r being Element of REAL holds b1 . r = - r ) & ( for r being Element of REAL holds b2 . r = - r ) holds
b1 = b2 from BINOP_2:sch 1( REAL REAL );
func invreal -> UnOp of REAL means :: BINOP_2:def 8
for r being Element of REAL holds it . r = r " ;
existence
ex b1 being UnOp of REAL st
for r being Element of REAL holds b1 . r = r " from FUNCT_2:sch 4( REAL REAL );
uniqueness
for b1, b2 being UnOp of REAL st ( for r being Element of REAL holds b1 . r = r " ) & ( for r being Element of REAL holds b2 . r = r " ) holds
b1 = b2 from BINOP_2:sch 1( REAL REAL );
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 b1 being BinOp of REAL st
for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 + r2 from BINOP_1:sch 2( REAL );
uniqueness
for b1, b2 being BinOp of REAL st ( for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 + r2 ) & ( for r1, r2 being Element of REAL holds b2 . r1,r2 = r1 + r2 ) holds
b1 = b2 from BINOP_2:sch 2( REAL );
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 b1 being BinOp of REAL st
for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 - r2 from BINOP_1:sch 2( REAL );
uniqueness
for b1, b2 being BinOp of REAL st ( for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 - r2 ) & ( for r1, r2 being Element of REAL holds b2 . r1,r2 = r1 - r2 ) holds
b1 = b2 from BINOP_2:sch 2( REAL );
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 b1 being BinOp of REAL st
for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 * r2 from BINOP_1:sch 2( REAL );
uniqueness
for b1, b2 being BinOp of REAL st ( for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 * r2 ) & ( for r1, r2 being Element of REAL holds b2 . r1,r2 = r1 * r2 ) holds
b1 = b2 from BINOP_2:sch 2( REAL );
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 b1 being BinOp of REAL st
for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 / r2 from BINOP_1:sch 2( REAL );
uniqueness
for b1, b2 being BinOp of REAL st ( for r1, r2 being Element of REAL holds b1 . r1,r2 = r1 / r2 ) & ( for r1, r2 being Element of REAL holds b2 . r1,r2 = r1 / r2 ) holds
b1 = b2 from BINOP_2:sch 2( REAL );
end;

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

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

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

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

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

:: deftheorem defines divreal BINOP_2:def 12 :
for b1 being BinOp of REAL holds
( b1 = divreal iff for r1, r2 being Element of REAL holds b1 . 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 b1 being UnOp of RAT st
for w being Element of RAT holds b1 . w = - w from FUNCT_2:sch 4( RAT RAT );
uniqueness
for b1, b2 being UnOp of RAT st ( for w being Element of RAT holds b1 . w = - w ) & ( for w being Element of RAT holds b2 . w = - w ) holds
b1 = b2 from BINOP_2:sch 1( RAT RAT );
func invrat -> UnOp of RAT means :: BINOP_2:def 14
for w being Element of RAT holds it . w = w " ;
existence
ex b1 being UnOp of RAT st
for w being Element of RAT holds b1 . w = w " from FUNCT_2:sch 4( RAT RAT );
uniqueness
for b1, b2 being UnOp of RAT st ( for w being Element of RAT holds b1 . w = w " ) & ( for w being Element of RAT holds b2 . w = w " ) holds
b1 = b2 from BINOP_2:sch 1( RAT RAT );
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 b1 being BinOp of RAT st
for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 + w2 from BINOP_1:sch 2( RAT );
uniqueness
for b1, b2 being BinOp of RAT st ( for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 + w2 ) & ( for w1, w2 being Element of RAT holds b2 . w1,w2 = w1 + w2 ) holds
b1 = b2 from BINOP_2:sch 2( RAT );
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 b1 being BinOp of RAT st
for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 - w2 from BINOP_1:sch 2( RAT );
uniqueness
for b1, b2 being BinOp of RAT st ( for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 - w2 ) & ( for w1, w2 being Element of RAT holds b2 . w1,w2 = w1 - w2 ) holds
b1 = b2 from BINOP_2:sch 2( RAT );
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 b1 being BinOp of RAT st
for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 * w2 from BINOP_1:sch 2( RAT );
uniqueness
for b1, b2 being BinOp of RAT st ( for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 * w2 ) & ( for w1, w2 being Element of RAT holds b2 . w1,w2 = w1 * w2 ) holds
b1 = b2 from BINOP_2:sch 2( RAT );
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 b1 being BinOp of RAT st
for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 / w2 from BINOP_1:sch 2( RAT );
uniqueness
for b1, b2 being BinOp of RAT st ( for w1, w2 being Element of RAT holds b1 . w1,w2 = w1 / w2 ) & ( for w1, w2 being Element of RAT holds b2 . w1,w2 = w1 / w2 ) holds
b1 = b2 from BINOP_2:sch 2( RAT );
end;

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

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

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

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

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

:: deftheorem defines divrat BINOP_2:def 18 :
for b1 being BinOp of RAT holds
( b1 = divrat iff for w1, w2 being Element of RAT holds b1 . 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 b1 being UnOp of INT st
for i being Element of INT holds b1 . i = - i from FUNCT_2:sch 4( INT INT );
uniqueness
for b1, b2 being UnOp of INT st ( for i being Element of INT holds b1 . i = - i ) & ( for i being Element of INT holds b2 . i = - i ) holds
b1 = b2 from BINOP_2:sch 1( INT INT );
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 b1 being BinOp of INT st
for i1, i2 being Element of INT holds b1 . i1,i2 = i1 + i2 from BINOP_1:sch 2( INT );
uniqueness
for b1, b2 being BinOp of INT st ( for i1, i2 being Element of INT holds b1 . i1,i2 = i1 + i2 ) & ( for i1, i2 being Element of INT holds b2 . i1,i2 = i1 + i2 ) holds
b1 = b2 from BINOP_2:sch 2( INT );
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 b1 being BinOp of INT st
for i1, i2 being Element of INT holds b1 . i1,i2 = i1 - i2 from BINOP_1:sch 2( INT );
uniqueness
for b1, b2 being BinOp of INT st ( for i1, i2 being Element of INT holds b1 . i1,i2 = i1 - i2 ) & ( for i1, i2 being Element of INT holds b2 . i1,i2 = i1 - i2 ) holds
b1 = b2 from BINOP_2:sch 2( INT );
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 b1 being BinOp of INT st
for i1, i2 being Element of INT holds b1 . i1,i2 = i1 * i2 from BINOP_1:sch 2( INT );
uniqueness
for b1, b2 being BinOp of INT st ( for i1, i2 being Element of INT holds b1 . i1,i2 = i1 * i2 ) & ( for i1, i2 being Element of INT holds b2 . i1,i2 = i1 * i2 ) holds
b1 = b2 from BINOP_2:sch 2( INT );
end;

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

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

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

:: deftheorem Def22 defines multint BINOP_2:def 22 :
for b1 being BinOp of INT holds
( b1 = multint iff for i1, i2 being Element of INT holds b1 . 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 b1 being BinOp of NAT st
for n1, n2 being Element of NAT holds b1 . n1,n2 = n1 + n2 from BINOP_1:sch 2( NAT );
uniqueness
for b1, b2 being BinOp of NAT st ( for n1, n2 being Element of NAT holds b1 . n1,n2 = n1 + n2 ) & ( for n1, n2 being Element of NAT holds b2 . n1,n2 = n1 + n2 ) holds
b1 = b2 from BINOP_2:sch 2( NAT );
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 b1 being BinOp of NAT st
for n1, n2 being Element of NAT holds b1 . n1,n2 = n1 * n2 from BINOP_1:sch 2( NAT );
uniqueness
for b1, b2 being BinOp of NAT st ( for n1, n2 being Element of NAT holds b1 . n1,n2 = n1 * n2 ) & ( for n1, n2 being Element of NAT holds b2 . n1,n2 = n1 * n2 ) holds
b1 = b2 from BINOP_2:sch 2( NAT );
end;

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

:: deftheorem Def24 defines multnat BINOP_2:def 24 :
for b1 being BinOp of NAT holds
( b1 = multnat iff for n1, n2 being Element of NAT holds b1 . 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 -> commutative associative having_a_unity ;
coherence
addcomplex is having_a_unity by Lm2, SETWISEO:def 2;
cluster addreal -> commutative associative having_a_unity ;
coherence
addreal is having_a_unity by Lm3, SETWISEO:def 2;
cluster addrat -> commutative associative having_a_unity ;
coherence
addrat is having_a_unity by Lm4, SETWISEO:def 2;
cluster addint -> commutative associative having_a_unity ;
coherence
addint is having_a_unity by Lm5, SETWISEO:def 2;
cluster addnat -> commutative associative having_a_unity ;
coherence
addnat is having_a_unity by Lm6, SETWISEO:def 2;
cluster multcomplex -> commutative associative having_a_unity ;
coherence
multcomplex is having_a_unity by Lm8, SETWISEO:def 2;
cluster multreal -> commutative associative having_a_unity ;
coherence
multreal is having_a_unity by Lm9, SETWISEO:def 2;
cluster multrat -> commutative associative having_a_unity ;
coherence
multrat is having_a_unity by Lm10, SETWISEO:def 2;
cluster multint -> commutative associative having_a_unity ;
coherence
multint is having_a_unity by Lm11, SETWISEO:def 2;
cluster multnat -> commutative associative having_a_unity ;
coherence
multnat is having_a_unity by Lm12, SETWISEO:def 2;
end;

theorem :: BINOP_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt addcomplex = 0 by Lm2, BINOP_1:def 8;

theorem :: BINOP_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt addreal = 0 by Lm3, BINOP_1:def 8;

theorem :: BINOP_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt addrat = 0 by Lm4, BINOP_1:def 8;

theorem :: BINOP_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt addint = 0 by Lm5, BINOP_1:def 8;

theorem :: BINOP_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt addnat = 0 by Lm6, BINOP_1:def 8;

theorem :: BINOP_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt multcomplex = 1 by Lm8, BINOP_1:def 8;

theorem :: BINOP_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt multreal = 1 by Lm9, BINOP_1:def 8;

theorem :: BINOP_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt multrat = 1 by Lm10, BINOP_1:def 8;

theorem :: BINOP_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt multint = 1 by Lm11, BINOP_1:def 8;

theorem :: BINOP_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt multnat = 1 by Lm12, BINOP_1:def 8;