:: by Library Committee

::

:: Received June 21, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

scheme :: BINOP_2:sch 1

FuncDefUniq{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( Element of F_{1}()) -> set } :

FuncDefUniq{ F

for f1, f2 being Function of F_{1}(),F_{2}() st ( for x being Element of F_{1}() holds f1 . x = F_{3}(x) ) & ( for x being Element of F_{1}() holds f2 . x = F_{3}(x) ) holds

f1 = f2

f1 = f2

proof end;

scheme :: BINOP_2:sch 2

BinOpDefuniq{ F_{1}() -> non empty set , F_{2}( Element of F_{1}(), Element of F_{1}()) -> set } :

BinOpDefuniq{ F

for o1, o2 being BinOp of F_{1}() st ( for a, b being Element of F_{1}() holds o1 . (a,b) = F_{2}(a,b) ) & ( for a, b being Element of F_{1}() holds o2 . (a,b) = F_{2}(a,b) ) holds

o1 = o2

o1 = o2

proof end;

definition

let c1 be complex number ;

:: 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 complex number ;

:: 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;
:: 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 complex number ;

:: 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;

definition

let r1 be real number ;

:: 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 real number ;

:: 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;
:: 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 real number ;

:: 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;

definition

let w1 be rational number ;

:: 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 rational number ;

:: 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;
:: 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 rational number ;

:: 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;

definition

let i1 be integer number ;

:: original: -

redefine func - i1 -> Element of INT ;

coherence

- i1 is Element of INT by INT_1:def 2;

let i2 be integer number ;

:: 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;
:: original: -

redefine func - i1 -> Element of INT ;

coherence

- i1 is Element of INT by INT_1:def 2;

let i2 be integer number ;

:: 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;

definition

let n1, n2 be Nat;

:: original: +

redefine func n1 + n2 -> Element of NAT ;

coherence

n1 + n2 is Element of NAT by ORDINAL1:def 12;

:: original: *

redefine func n1 * n2 -> Element of NAT ;

coherence

n1 * n2 is Element of NAT by ORDINAL1:def 12;

end;
:: original: +

redefine func n1 + n2 -> Element of NAT ;

coherence

n1 + n2 is Element of NAT by ORDINAL1:def 12;

:: original: *

redefine func n1 * n2 -> Element of NAT ;

coherence

n1 * n2 is Element of NAT by ORDINAL1:def 12;

definition

ex b_{1} being UnOp of COMPLEX st

for c being complex number holds b_{1} . c = - c
from BINOP_2:sch 18();

uniqueness

for b_{1}, b_{2} being UnOp of COMPLEX st ( for c being complex number holds b_{1} . c = - c ) & ( for c being complex number holds b_{2} . c = - c ) holds

b_{1} = b_{2}
from BINOP_2:sch 3();

ex b_{1} being UnOp of COMPLEX st

for c being complex number holds b_{1} . c = c "
from BINOP_2:sch 18();

uniqueness

for b_{1}, b_{2} being UnOp of COMPLEX st ( for c being complex number holds b_{1} . c = c " ) & ( for c being complex number holds b_{2} . c = c " ) holds

b_{1} = b_{2}
from BINOP_2:sch 3();

ex b_{1} being BinOp of COMPLEX st

for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 + c2
from BINOP_2:sch 13();

uniqueness

for b_{1}, b_{2} being BinOp of COMPLEX st ( for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 + c2 ) & ( for c1, c2 being complex number holds b_{2} . (c1,c2) = c1 + c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 8();

ex b_{1} being BinOp of COMPLEX st

for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 - c2
from BINOP_2:sch 13();

uniqueness

for b_{1}, b_{2} being BinOp of COMPLEX st ( for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 - c2 ) & ( for c1, c2 being complex number holds b_{2} . (c1,c2) = c1 - c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 8();

ex b_{1} being BinOp of COMPLEX st

for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 * c2
from BINOP_2:sch 13();

uniqueness

for b_{1}, b_{2} being BinOp of COMPLEX st ( for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 * c2 ) & ( for c1, c2 being complex number holds b_{2} . (c1,c2) = c1 * c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 8();

ex b_{1} being BinOp of COMPLEX st

for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 / c2
from BINOP_2:sch 13();

uniqueness

for b_{1}, b_{2} being BinOp of COMPLEX st ( for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 / c2 ) & ( for c1, c2 being complex number holds b_{2} . (c1,c2) = c1 / c2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 8();

end;

func compcomplex -> UnOp of COMPLEX means :: BINOP_2:def 1

for c being complex number holds it . c = - c;

existence for c being complex number holds it . c = - c;

ex b

for c being complex number holds b

uniqueness

for b

b

func invcomplex -> UnOp of COMPLEX means :: BINOP_2:def 2

for c being complex number holds it . c = c " ;

existence for c being complex number holds it . c = c " ;

ex b

for c being complex number holds b

uniqueness

for b

b

func addcomplex -> BinOp of COMPLEX means :Def3: :: BINOP_2:def 3

for c1, c2 being complex number holds it . (c1,c2) = c1 + c2;

existence for c1, c2 being complex number holds it . (c1,c2) = c1 + c2;

ex b

for c1, c2 being complex number holds b

uniqueness

for b

b

func diffcomplex -> BinOp of COMPLEX means :: BINOP_2:def 4

for c1, c2 being complex number holds it . (c1,c2) = c1 - c2;

existence for c1, c2 being complex number holds it . (c1,c2) = c1 - c2;

ex b

for c1, c2 being complex number holds b

uniqueness

for b

b

func multcomplex -> BinOp of COMPLEX means :Def5: :: BINOP_2:def 5

for c1, c2 being complex number holds it . (c1,c2) = c1 * c2;

existence for c1, c2 being complex number holds it . (c1,c2) = c1 * c2;

ex b

for c1, c2 being complex number holds b

uniqueness

for b

b

func divcomplex -> BinOp of COMPLEX means :: BINOP_2:def 6

for c1, c2 being complex number holds it . (c1,c2) = c1 / c2;

existence for c1, c2 being complex number holds it . (c1,c2) = c1 / c2;

ex b

for c1, c2 being complex number holds b

uniqueness

for b

b

:: deftheorem defines compcomplex BINOP_2:def 1 :

for b_{1} being UnOp of COMPLEX holds

( b_{1} = compcomplex iff for c being complex number holds b_{1} . c = - c );

for b

( b

:: deftheorem defines invcomplex BINOP_2:def 2 :

for b_{1} being UnOp of COMPLEX holds

( b_{1} = invcomplex iff for c being complex number holds b_{1} . c = c " );

for b

( b

:: deftheorem Def3 defines addcomplex BINOP_2:def 3 :

for b_{1} being BinOp of COMPLEX holds

( b_{1} = addcomplex iff for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 + c2 );

for b

( b

:: deftheorem defines diffcomplex BINOP_2:def 4 :

for b_{1} being BinOp of COMPLEX holds

( b_{1} = diffcomplex iff for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 - c2 );

for b

( b

:: deftheorem Def5 defines multcomplex BINOP_2:def 5 :

for b_{1} being BinOp of COMPLEX holds

( b_{1} = multcomplex iff for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 * c2 );

for b

( b

:: deftheorem defines divcomplex BINOP_2:def 6 :

for b_{1} being BinOp of COMPLEX holds

( b_{1} = divcomplex iff for c1, c2 being complex number holds b_{1} . (c1,c2) = c1 / c2 );

for b

( b

definition

existence

ex b_{1} being UnOp of REAL st

for r being real number holds b_{1} . r = - r
from BINOP_2:sch 19();

uniqueness

for b_{1}, b_{2} being UnOp of REAL st ( for r being real number holds b_{1} . r = - r ) & ( for r being real number holds b_{2} . r = - r ) holds

b_{1} = b_{2}
from BINOP_2:sch 4();

existence

ex b_{1} being UnOp of REAL st

for r being real number holds b_{1} . r = r "
from BINOP_2:sch 19();

uniqueness

for b_{1}, b_{2} being UnOp of REAL st ( for r being real number holds b_{1} . r = r " ) & ( for r being real number holds b_{2} . r = r " ) holds

b_{1} = b_{2}
from BINOP_2:sch 4();

ex b_{1} being BinOp of REAL st

for r1, r2 being real number holds b_{1} . (r1,r2) = r1 + r2
from BINOP_2:sch 14();

uniqueness

for b_{1}, b_{2} being BinOp of REAL st ( for r1, r2 being real number holds b_{1} . (r1,r2) = r1 + r2 ) & ( for r1, r2 being real number holds b_{2} . (r1,r2) = r1 + r2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 9();

ex b_{1} being BinOp of REAL st

for r1, r2 being real number holds b_{1} . (r1,r2) = r1 - r2
from BINOP_2:sch 14();

uniqueness

for b_{1}, b_{2} being BinOp of REAL st ( for r1, r2 being real number holds b_{1} . (r1,r2) = r1 - r2 ) & ( for r1, r2 being real number holds b_{2} . (r1,r2) = r1 - r2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 9();

ex b_{1} being BinOp of REAL st

for r1, r2 being real number holds b_{1} . (r1,r2) = r1 * r2
from BINOP_2:sch 14();

uniqueness

for b_{1}, b_{2} being BinOp of REAL st ( for r1, r2 being real number holds b_{1} . (r1,r2) = r1 * r2 ) & ( for r1, r2 being real number holds b_{2} . (r1,r2) = r1 * r2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 9();

ex b_{1} being BinOp of REAL st

for r1, r2 being real number holds b_{1} . (r1,r2) = r1 / r2
from BINOP_2:sch 14();

uniqueness

for b_{1}, b_{2} being BinOp of REAL st ( for r1, r2 being real number holds b_{1} . (r1,r2) = r1 / r2 ) & ( for r1, r2 being real number holds b_{2} . (r1,r2) = r1 / r2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 9();

end;
ex b

for r being real number holds b

uniqueness

for b

b

existence

ex b

for r being real number holds b

uniqueness

for b

b

func addreal -> BinOp of REAL means :Def9: :: BINOP_2:def 9

for r1, r2 being real number holds it . (r1,r2) = r1 + r2;

existence for r1, r2 being real number holds it . (r1,r2) = r1 + r2;

ex b

for r1, r2 being real number holds b

uniqueness

for b

b

func diffreal -> BinOp of REAL means :: BINOP_2:def 10

for r1, r2 being real number holds it . (r1,r2) = r1 - r2;

existence for r1, r2 being real number holds it . (r1,r2) = r1 - r2;

ex b

for r1, r2 being real number holds b

uniqueness

for b

b

func multreal -> BinOp of REAL means :Def11: :: BINOP_2:def 11

for r1, r2 being real number holds it . (r1,r2) = r1 * r2;

existence for r1, r2 being real number holds it . (r1,r2) = r1 * r2;

ex b

for r1, r2 being real number holds b

uniqueness

for b

b

func divreal -> BinOp of REAL means :: BINOP_2:def 12

for r1, r2 being real number holds it . (r1,r2) = r1 / r2;

existence for r1, r2 being real number holds it . (r1,r2) = r1 / r2;

ex b

for r1, r2 being real number holds b

uniqueness

for b

b

:: deftheorem defines compreal BINOP_2:def 7 :

for b_{1} being UnOp of REAL holds

( b_{1} = compreal iff for r being real number holds b_{1} . r = - r );

for b

( b

:: deftheorem defines invreal BINOP_2:def 8 :

for b_{1} being UnOp of REAL holds

( b_{1} = invreal iff for r being real number holds b_{1} . r = r " );

for b

( b

:: deftheorem Def9 defines addreal BINOP_2:def 9 :

for b_{1} being BinOp of REAL holds

( b_{1} = addreal iff for r1, r2 being real number holds b_{1} . (r1,r2) = r1 + r2 );

for b

( b

:: deftheorem defines diffreal BINOP_2:def 10 :

for b_{1} being BinOp of REAL holds

( b_{1} = diffreal iff for r1, r2 being real number holds b_{1} . (r1,r2) = r1 - r2 );

for b

( b

:: deftheorem Def11 defines multreal BINOP_2:def 11 :

for b_{1} being BinOp of REAL holds

( b_{1} = multreal iff for r1, r2 being real number holds b_{1} . (r1,r2) = r1 * r2 );

for b

( b

:: deftheorem defines divreal BINOP_2:def 12 :

for b_{1} being BinOp of REAL holds

( b_{1} = divreal iff for r1, r2 being real number holds b_{1} . (r1,r2) = r1 / r2 );

for b

( b

definition

existence

ex b_{1} being UnOp of RAT st

for w being rational number holds b_{1} . w = - w
from BINOP_2:sch 20();

uniqueness

for b_{1}, b_{2} being UnOp of RAT st ( for w being rational number holds b_{1} . w = - w ) & ( for w being rational number holds b_{2} . w = - w ) holds

b_{1} = b_{2}
from BINOP_2:sch 5();

existence

ex b_{1} being UnOp of RAT st

for w being rational number holds b_{1} . w = w "
from BINOP_2:sch 20();

uniqueness

for b_{1}, b_{2} being UnOp of RAT st ( for w being rational number holds b_{1} . w = w " ) & ( for w being rational number holds b_{2} . w = w " ) holds

b_{1} = b_{2}
from BINOP_2:sch 5();

ex b_{1} being BinOp of RAT st

for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 + w2
from BINOP_2:sch 15();

uniqueness

for b_{1}, b_{2} being BinOp of RAT st ( for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 + w2 ) & ( for w1, w2 being rational number holds b_{2} . (w1,w2) = w1 + w2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 10();

ex b_{1} being BinOp of RAT st

for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 - w2
from BINOP_2:sch 15();

uniqueness

for b_{1}, b_{2} being BinOp of RAT st ( for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 - w2 ) & ( for w1, w2 being rational number holds b_{2} . (w1,w2) = w1 - w2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 10();

ex b_{1} being BinOp of RAT st

for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 * w2
from BINOP_2:sch 15();

uniqueness

for b_{1}, b_{2} being BinOp of RAT st ( for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 * w2 ) & ( for w1, w2 being rational number holds b_{2} . (w1,w2) = w1 * w2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 10();

ex b_{1} being BinOp of RAT st

for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 / w2
from BINOP_2:sch 15();

uniqueness

for b_{1}, b_{2} being BinOp of RAT st ( for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 / w2 ) & ( for w1, w2 being rational number holds b_{2} . (w1,w2) = w1 / w2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 10();

end;
ex b

for w being rational number holds b

uniqueness

for b

b

existence

ex b

for w being rational number holds b

uniqueness

for b

b

func addrat -> BinOp of RAT means :Def15: :: BINOP_2:def 15

for w1, w2 being rational number holds it . (w1,w2) = w1 + w2;

existence for w1, w2 being rational number holds it . (w1,w2) = w1 + w2;

ex b

for w1, w2 being rational number holds b

uniqueness

for b

b

func diffrat -> BinOp of RAT means :: BINOP_2:def 16

for w1, w2 being rational number holds it . (w1,w2) = w1 - w2;

existence for w1, w2 being rational number holds it . (w1,w2) = w1 - w2;

ex b

for w1, w2 being rational number holds b

uniqueness

for b

b

func multrat -> BinOp of RAT means :Def17: :: BINOP_2:def 17

for w1, w2 being rational number holds it . (w1,w2) = w1 * w2;

existence for w1, w2 being rational number holds it . (w1,w2) = w1 * w2;

ex b

for w1, w2 being rational number holds b

uniqueness

for b

b

func divrat -> BinOp of RAT means :: BINOP_2:def 18

for w1, w2 being rational number holds it . (w1,w2) = w1 / w2;

existence for w1, w2 being rational number holds it . (w1,w2) = w1 / w2;

ex b

for w1, w2 being rational number holds b

uniqueness

for b

b

:: deftheorem defines comprat BINOP_2:def 13 :

for b_{1} being UnOp of RAT holds

( b_{1} = comprat iff for w being rational number holds b_{1} . w = - w );

for b

( b

:: deftheorem defines invrat BINOP_2:def 14 :

for b_{1} being UnOp of RAT holds

( b_{1} = invrat iff for w being rational number holds b_{1} . w = w " );

for b

( b

:: deftheorem Def15 defines addrat BINOP_2:def 15 :

for b_{1} being BinOp of RAT holds

( b_{1} = addrat iff for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 + w2 );

for b

( b

:: deftheorem defines diffrat BINOP_2:def 16 :

for b_{1} being BinOp of RAT holds

( b_{1} = diffrat iff for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 - w2 );

for b

( b

:: deftheorem Def17 defines multrat BINOP_2:def 17 :

for b_{1} being BinOp of RAT holds

( b_{1} = multrat iff for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 * w2 );

for b

( b

:: deftheorem defines divrat BINOP_2:def 18 :

for b_{1} being BinOp of RAT holds

( b_{1} = divrat iff for w1, w2 being rational number holds b_{1} . (w1,w2) = w1 / w2 );

for b

( b

definition

existence

ex b_{1} being UnOp of INT st

for i being integer number holds b_{1} . i = - i
from BINOP_2:sch 21();

uniqueness

for b_{1}, b_{2} being UnOp of INT st ( for i being integer number holds b_{1} . i = - i ) & ( for i being integer number holds b_{2} . i = - i ) holds

b_{1} = b_{2}
from BINOP_2:sch 6();

ex b_{1} being BinOp of INT st

for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 + i2
from BINOP_2:sch 16();

uniqueness

for b_{1}, b_{2} being BinOp of INT st ( for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 + i2 ) & ( for i1, i2 being integer number holds b_{2} . (i1,i2) = i1 + i2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 11();

ex b_{1} being BinOp of INT st

for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 - i2
from BINOP_2:sch 16();

uniqueness

for b_{1}, b_{2} being BinOp of INT st ( for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 - i2 ) & ( for i1, i2 being integer number holds b_{2} . (i1,i2) = i1 - i2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 11();

ex b_{1} being BinOp of INT st

for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 * i2
from BINOP_2:sch 16();

uniqueness

for b_{1}, b_{2} being BinOp of INT st ( for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 * i2 ) & ( for i1, i2 being integer number holds b_{2} . (i1,i2) = i1 * i2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 11();

end;
ex b

for i being integer number holds b

uniqueness

for b

b

func addint -> BinOp of INT means :Def20: :: BINOP_2:def 20

for i1, i2 being integer number holds it . (i1,i2) = i1 + i2;

existence for i1, i2 being integer number holds it . (i1,i2) = i1 + i2;

ex b

for i1, i2 being integer number holds b

uniqueness

for b

b

func diffint -> BinOp of INT means :: BINOP_2:def 21

for i1, i2 being integer number holds it . (i1,i2) = i1 - i2;

existence for i1, i2 being integer number holds it . (i1,i2) = i1 - i2;

ex b

for i1, i2 being integer number holds b

uniqueness

for b

b

func multint -> BinOp of INT means :Def22: :: BINOP_2:def 22

for i1, i2 being integer number holds it . (i1,i2) = i1 * i2;

existence for i1, i2 being integer number holds it . (i1,i2) = i1 * i2;

ex b

for i1, i2 being integer number holds b

uniqueness

for b

b

:: deftheorem defines compint BINOP_2:def 19 :

for b_{1} being UnOp of INT holds

( b_{1} = compint iff for i being integer number holds b_{1} . i = - i );

for b

( b

:: deftheorem Def20 defines addint BINOP_2:def 20 :

for b_{1} being BinOp of INT holds

( b_{1} = addint iff for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 + i2 );

for b

( b

:: deftheorem defines diffint BINOP_2:def 21 :

for b_{1} being BinOp of INT holds

( b_{1} = diffint iff for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 - i2 );

for b

( b

:: deftheorem Def22 defines multint BINOP_2:def 22 :

for b_{1} being BinOp of INT holds

( b_{1} = multint iff for i1, i2 being integer number holds b_{1} . (i1,i2) = i1 * i2 );

for b

( b

definition

ex b_{1} being BinOp of NAT st

for n1, n2 being Nat holds b_{1} . (n1,n2) = n1 + n2
from BINOP_2:sch 17();

uniqueness

for b_{1}, b_{2} being BinOp of NAT st ( for n1, n2 being Nat holds b_{1} . (n1,n2) = n1 + n2 ) & ( for n1, n2 being Nat holds b_{2} . (n1,n2) = n1 + n2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 12();

ex b_{1} being BinOp of NAT st

for n1, n2 being Nat holds b_{1} . (n1,n2) = n1 * n2
from BINOP_2:sch 17();

uniqueness

for b_{1}, b_{2} being BinOp of NAT st ( for n1, n2 being Nat holds b_{1} . (n1,n2) = n1 * n2 ) & ( for n1, n2 being Nat holds b_{2} . (n1,n2) = n1 * n2 ) holds

b_{1} = b_{2}
from BINOP_2:sch 12();

end;

func addnat -> BinOp of NAT means :Def23: :: BINOP_2:def 23

for n1, n2 being Nat holds it . (n1,n2) = n1 + n2;

existence for n1, n2 being Nat holds it . (n1,n2) = n1 + n2;

ex b

for n1, n2 being Nat holds b

uniqueness

for b

b

func multnat -> BinOp of NAT means :Def24: :: BINOP_2:def 24

for n1, n2 being Nat holds it . (n1,n2) = n1 * n2;

existence for n1, n2 being Nat holds it . (n1,n2) = n1 * n2;

ex b

for n1, n2 being Nat holds b

uniqueness

for b

b

:: deftheorem Def23 defines addnat BINOP_2:def 23 :

for b_{1} being BinOp of NAT holds

( b_{1} = addnat iff for n1, n2 being Nat holds b_{1} . (n1,n2) = n1 + n2 );

for b

( b

:: deftheorem Def24 defines multnat BINOP_2:def 24 :

for b_{1} being BinOp of NAT holds

( b_{1} = multnat iff for n1, n2 being Nat holds b_{1} . (n1,n2) = n1 * n2 );

for b

( b

registration

coherence

( addcomplex is commutative & addcomplex is associative )

( multcomplex is commutative & multcomplex is associative )

( addreal is commutative & addreal is associative )

( multreal is commutative & multreal is associative )

( addrat is commutative & addrat is associative )

( multrat is commutative & multrat is associative )

( addint is commutative & addint is associative )

( multint is commutative & multint is associative )

( addnat is commutative & addnat is associative )

( multnat is commutative & multnat is associative )

end;
( addcomplex is commutative & addcomplex is associative )

proof end;

coherence ( multcomplex is commutative & multcomplex is associative )

proof end;

coherence ( addreal is commutative & addreal is associative )

proof end;

coherence ( multreal is commutative & multreal is associative )

proof end;

coherence ( addrat is commutative & addrat is associative )

proof end;

coherence ( multrat is commutative & multrat is associative )

proof end;

coherence ( addint is commutative & addint is associative )

proof end;

coherence ( multint is commutative & multint is associative )

proof end;

coherence ( addnat is commutative & addnat is associative )

proof end;

coherence ( multnat is commutative & multnat is associative )

proof 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

coherence

addcomplex is having_a_unity by Lm2, SETWISEO:def 2;

coherence

addreal is having_a_unity by Lm3, SETWISEO:def 2;

coherence

addrat is having_a_unity by Lm4, SETWISEO:def 2;

coherence

addint is having_a_unity by Lm5, SETWISEO:def 2;

coherence

addnat is having_a_unity by Lm6, SETWISEO:def 2;

coherence

multcomplex is having_a_unity by Lm8, SETWISEO:def 2;

coherence

multreal is having_a_unity by Lm9, SETWISEO:def 2;

coherence

multrat is having_a_unity by Lm10, SETWISEO:def 2;

coherence

multint is having_a_unity by Lm11, SETWISEO:def 2;

coherence

multnat is having_a_unity by Lm12, SETWISEO:def 2;

end;
addcomplex is having_a_unity by Lm2, SETWISEO:def 2;

coherence

addreal is having_a_unity by Lm3, SETWISEO:def 2;

coherence

addrat is having_a_unity by Lm4, SETWISEO:def 2;

coherence

addint is having_a_unity by Lm5, SETWISEO:def 2;

coherence

addnat is having_a_unity by Lm6, SETWISEO:def 2;

coherence

multcomplex is having_a_unity by Lm8, SETWISEO:def 2;

coherence

multreal is having_a_unity by Lm9, SETWISEO:def 2;

coherence

multrat is having_a_unity by Lm10, SETWISEO:def 2;

coherence

multint is having_a_unity by Lm11, SETWISEO:def 2;

coherence

multnat is having_a_unity by Lm12, SETWISEO:def 2;