binop_2.miz



    begin

    scheme :: BINOP_2:sch1

    FuncDefUniq { C,D() -> non empty set , F( Element of C()) -> object } :

for f1,f2 be Function of C(), D() st (for x be Element of C() holds (f1 . x) = F(x)) & (for x be Element of C() holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be Function of C(), D() such that

       A1: for x be Element of C() holds (f1 . x) = F(x) and

       A2: for x be Element of C() holds (f2 . x) = F(x);

      now

        let x be Element of C();

        

        thus (f1 . x) = F(x) by A1

        .= (f2 . x) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: BINOP_2:sch2

    BinOpDefuniq { A() -> non empty set , O( Element of A(), Element of A()) -> object } :

for o1,o2 be BinOp of A() st (for a,b be Element of A() holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of A() holds (o2 . (a,b)) = O(a,b)) holds o1 = o2;

      let o1,o2 be BinOp of A() such that

       A1: for a,b be Element of A() holds (o1 . (a,b)) = O(a,b) and

       A2: for a,b be Element of A() holds (o2 . (a,b)) = O(a,b);

      now

        let a,b be Element of A();

        

        thus (o1 . (a,b)) = O(a,b) by A1

        .= (o2 . (a,b)) by A2;

      end;

      hence thesis;

    end;

    scheme :: BINOP_2:sch3

    CFuncDefUniq { F( object) -> object } :

for f1,f2 be Function of COMPLEX , COMPLEX st (for x be Complex holds (f1 . x) = F(x)) & (for x be Complex holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be Function of COMPLEX , COMPLEX such that

       A1: for x be Complex holds (f1 . x) = F(x) and

       A2: for x be Complex holds (f2 . x) = F(x);

      now

        let x be Element of COMPLEX ;

        

        thus (f1 . x) = F(x) by A1

        .= (f2 . x) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: BINOP_2:sch4

    RFuncDefUniq { F( Real) -> object } :

for f1,f2 be Function of REAL , REAL st (for x be Real holds (f1 . x) = F(x)) & (for x be Real holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be Function of REAL , REAL such that

       A1: for x be Real holds (f1 . x) = F(x) and

       A2: for x be Real holds (f2 . x) = F(x);

      now

        let x be Element of REAL ;

        

        thus (f1 . x) = F(x) by A1

        .= (f2 . x) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

      cluster -> rational for Element of RAT ;

      coherence by RAT_1:def 2;

    end

    scheme :: BINOP_2:sch5

    WFuncDefUniq { F( Rational) -> object } :

for f1,f2 be Function of RAT , RAT st (for x be Rational holds (f1 . x) = F(x)) & (for x be Rational holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be Function of RAT , RAT such that

       A1: for x be Rational holds (f1 . x) = F(x) and

       A2: for x be Rational holds (f2 . x) = F(x);

      now

        let x be Element of RAT ;

        

        thus (f1 . x) = F(x) by A1

        .= (f2 . x) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: BINOP_2:sch6

    IFuncDefUniq { F( Integer) -> object } :

for f1,f2 be Function of INT , INT st (for x be Integer holds (f1 . x) = F(x)) & (for x be Integer holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be Function of INT , INT such that

       A1: for x be Integer holds (f1 . x) = F(x) and

       A2: for x be Integer holds (f2 . x) = F(x);

      now

        let x be Element of INT ;

        

        thus (f1 . x) = F(x) by A1

        .= (f2 . x) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: BINOP_2:sch7

    NFuncDefUniq { F( Nat) -> object } :

for f1,f2 be sequence of NAT st (for x be Nat holds (f1 . x) = F(x)) & (for x be Nat holds (f2 . x) = F(x)) holds f1 = f2;

      let f1,f2 be sequence of NAT such that

       A1: for x be Nat holds (f1 . x) = F(x) and

       A2: for x be Nat holds (f2 . x) = F(x);

      now

        let x be Element of NAT ;

        

        thus (f1 . x) = F(x) by A1

        .= (f2 . x) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: BINOP_2:sch8

    CBinOpDefuniq { O( Complex, Complex) -> object } :

for o1,o2 be BinOp of COMPLEX st (for a,b be Complex holds (o1 . (a,b)) = O(a,b)) & (for a,b be Complex holds (o2 . (a,b)) = O(a,b)) holds o1 = o2;

      let o1,o2 be BinOp of COMPLEX such that

       A1: for a,b be Complex holds (o1 . (a,b)) = O(a,b) and

       A2: for a,b be Complex holds (o2 . (a,b)) = O(a,b);

      now

        let a,b be Element of COMPLEX ;

        

        thus (o1 . (a,b)) = O(a,b) by A1

        .= (o2 . (a,b)) by A2;

      end;

      hence thesis;

    end;

    scheme :: BINOP_2:sch9

    RBinOpDefuniq { O( Real, Real) -> object } :

for o1,o2 be BinOp of REAL st (for a,b be Real holds (o1 . (a,b)) = O(a,b)) & (for a,b be Real holds (o2 . (a,b)) = O(a,b)) holds o1 = o2;

      let o1,o2 be BinOp of REAL such that

       A1: for a,b be Real holds (o1 . (a,b)) = O(a,b) and

       A2: for a,b be Real holds (o2 . (a,b)) = O(a,b);

      now

        let a,b be Element of REAL ;

        

        thus (o1 . (a,b)) = O(a,b) by A1

        .= (o2 . (a,b)) by A2;

      end;

      hence thesis;

    end;

    scheme :: BINOP_2:sch10

    WBinOpDefuniq { O( Rational, Rational) -> object } :

for o1,o2 be BinOp of RAT st (for a,b be Rational holds (o1 . (a,b)) = O(a,b)) & (for a,b be Rational holds (o2 . (a,b)) = O(a,b)) holds o1 = o2;

      let o1,o2 be BinOp of RAT such that

       A1: for a,b be Rational holds (o1 . (a,b)) = O(a,b) and

       A2: for a,b be Rational holds (o2 . (a,b)) = O(a,b);

      now

        let a,b be Element of RAT ;

        

        thus (o1 . (a,b)) = O(a,b) by A1

        .= (o2 . (a,b)) by A2;

      end;

      hence thesis;

    end;

    scheme :: BINOP_2:sch11

    IBinOpDefuniq { O( Integer, Integer) -> object } :

for o1,o2 be BinOp of INT st (for a,b be Integer holds (o1 . (a,b)) = O(a,b)) & (for a,b be Integer holds (o2 . (a,b)) = O(a,b)) holds o1 = o2;

      let o1,o2 be BinOp of INT such that

       A1: for a,b be Integer holds (o1 . (a,b)) = O(a,b) and

       A2: for a,b be Integer holds (o2 . (a,b)) = O(a,b);

      now

        let a,b be Element of INT ;

        

        thus (o1 . (a,b)) = O(a,b) by A1

        .= (o2 . (a,b)) by A2;

      end;

      hence thesis;

    end;

    scheme :: BINOP_2:sch12

    NBinOpDefuniq { O( Nat, Nat) -> object } :

for o1,o2 be BinOp of NAT st (for a,b be Nat holds (o1 . (a,b)) = O(a,b)) & (for a,b be Nat holds (o2 . (a,b)) = O(a,b)) holds o1 = o2;

      let o1,o2 be BinOp of NAT such that

       A1: for a,b be Nat holds (o1 . (a,b)) = O(a,b) and

       A2: for a,b be Nat holds (o2 . (a,b)) = O(a,b);

      now

        let a,b be Element of NAT ;

        

        thus (o1 . (a,b)) = O(a,b) by A1

        .= (o2 . (a,b)) by A2;

      end;

      hence thesis;

    end;

    scheme :: BINOP_2:sch13

    CLambda2D { F( Complex, Complex) -> Complex } :

ex f be Function of [: COMPLEX , COMPLEX :], COMPLEX st for x,y be Complex holds (f . (x,y)) = F(x,y);

      defpred P[ Complex, Complex, set] means $3 = F($1,$2);

      

       A1: for x,y be Element of COMPLEX holds ex z be Element of COMPLEX st P[x, y, z]

      proof

        let x,y be Element of COMPLEX ;

        reconsider z = F(x,y) as Element of COMPLEX by XCMPLX_0:def 2;

        take z;

        thus P[x, y, z];

      end;

      consider f be Function of [: COMPLEX , COMPLEX :], COMPLEX such that

       A2: for x,y be Element of COMPLEX holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

      take f;

      let x,y be Complex;

      reconsider x, y as Element of COMPLEX by XCMPLX_0:def 2;

       P[x, y, (f . (x,y))] by A2;

      then (f . (x,y)) = F(x,y);

      hence thesis;

    end;

    scheme :: BINOP_2:sch14

    RLambda2D { F( Real, Real) -> Real } :

ex f be Function of [: REAL , REAL :], REAL st for x,y be Real holds (f . (x,y)) = F(x,y);

      defpred P[ Real, Real, set] means $3 = F($1,$2);

      

       A1: for x,y be Element of REAL holds ex z be Element of REAL st P[x, y, z]

      proof

        let x,y be Element of REAL ;

        reconsider z = F(x,y) as Element of REAL by XREAL_0:def 1;

        take z;

        thus P[x, y, z];

      end;

      consider f be Function of [: REAL , REAL :], REAL such that

       A2: for x,y be Element of REAL holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

      take f;

      let x,y be Real;

      reconsider x, y as Element of REAL by XREAL_0:def 1;

       P[x, y, (f . (x,y))] by A2;

      then (f . (x,y)) = F(x,y);

      hence thesis;

    end;

    scheme :: BINOP_2:sch15

    WLambda2D { F( Rational, Rational) -> Rational } :

ex f be Function of [: RAT , RAT :], RAT st for x,y be Rational holds (f . (x,y)) = F(x,y);

      defpred P[ Rational, Rational, set] means $3 = F($1,$2);

      

       A1: for x,y be Element of RAT holds ex z be Element of RAT st P[x, y, z]

      proof

        let x,y be Element of RAT ;

        reconsider z = F(x,y) as Element of RAT by RAT_1:def 2;

        take z;

        thus P[x, y, z];

      end;

      consider f be Function of [: RAT , RAT :], RAT such that

       A2: for x,y be Element of RAT holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

      take f;

      let x,y be Rational;

      reconsider x, y as Element of RAT by RAT_1:def 2;

       P[x, y, (f . (x,y))] by A2;

      then (f . (x,y)) = F(x,y);

      hence thesis;

    end;

    scheme :: BINOP_2:sch16

    ILambda2D { F( Integer, Integer) -> Integer } :

ex f be Function of [: INT , INT :], INT st for x,y be Integer holds (f . (x,y)) = F(x,y);

      defpred P[ Integer, Integer, set] means $3 = F($1,$2);

      

       A1: for x,y be Element of INT holds ex z be Element of INT st P[x, y, z]

      proof

        let x,y be Element of INT ;

        reconsider z = F(x,y) as Element of INT by INT_1:def 2;

        take z;

        thus P[x, y, z];

      end;

      consider f be Function of [: INT , INT :], INT such that

       A2: for x,y be Element of INT holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

      take f;

      let x,y be Integer;

      reconsider x, y as Element of INT by INT_1:def 2;

       P[x, y, (f . (x,y))] by A2;

      then (f . (x,y)) = F(x,y);

      hence thesis;

    end;

    scheme :: BINOP_2:sch17

    NLambda2D { F( Nat, Nat) -> Nat } :

ex f be Function of [: NAT , NAT :], NAT st for x,y be Nat holds (f . (x,y)) = F(x,y);

      defpred P[ Nat, Nat, set] means $3 = F($1,$2);

      

       A1: for x,y be Element of NAT holds ex z be Element of NAT st P[x, y, z]

      proof

        let x,y be Element of NAT ;

        reconsider z = F(x,y) as Element of NAT by ORDINAL1:def 12;

        take z;

        thus P[x, y, z];

      end;

      consider f be Function of [: NAT , NAT :], NAT such that

       A2: for x,y be Element of NAT holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

      take f;

      let x,y be Nat;

      reconsider x, y as Element of NAT by ORDINAL1:def 12;

       P[x, y, (f . (x,y))] by A2;

      then (f . (x,y)) = F(x,y);

      hence thesis;

    end;

    scheme :: BINOP_2:sch18

    CLambdaD { F( Complex) -> Complex } :

ex f be Function of COMPLEX , COMPLEX st for x be Complex holds (f . x) = F(x);

      defpred P[ Element of COMPLEX , set] means $2 = F($1);

      

       A1: for x be Element of COMPLEX holds ex y be Element of COMPLEX st P[x, y]

      proof

        let x be Element of COMPLEX ;

        reconsider y = F(x) as Element of COMPLEX by XCMPLX_0:def 2;

        take y;

        thus P[x, y];

      end;

      consider f be Function of COMPLEX , COMPLEX such that

       A2: for x be Element of COMPLEX holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      let c be Complex;

      reconsider c as Element of COMPLEX by XCMPLX_0:def 2;

       P[c, (f . c)] by A2;

      hence thesis;

    end;

    scheme :: BINOP_2:sch19

    RLambdaD { F( Real) -> Real } :

ex f be Function of REAL , REAL st for x be Real holds (f . x) = F(x);

      defpred P[ Element of REAL , set] means $2 = F($1);

      

       A1: for x be Element of REAL holds ex y be Element of REAL st P[x, y]

      proof

        let x be Element of REAL ;

        reconsider y = F(x) as Element of REAL by XREAL_0:def 1;

        take y;

        thus P[x, y];

      end;

      consider f be Function of REAL , REAL such that

       A2: for x be Element of REAL holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      let c be Real;

      reconsider c as Element of REAL by XREAL_0:def 1;

       P[c, (f . c)] by A2;

      hence thesis;

    end;

    scheme :: BINOP_2:sch20

    WLambdaD { F( Rational) -> Rational } :

ex f be Function of RAT , RAT st for x be Rational holds (f . x) = F(x);

      defpred P[ Element of RAT , set] means $2 = F($1);

      

       A1: for x be Element of RAT holds ex y be Element of RAT st P[x, y]

      proof

        let x be Element of RAT ;

        reconsider y = F(x) as Element of RAT by RAT_1:def 2;

        take y;

        thus P[x, y];

      end;

      consider f be Function of RAT , RAT such that

       A2: for x be Element of RAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      let c be Rational;

      reconsider c as Element of RAT by RAT_1:def 2;

       P[c, (f . c)] by A2;

      hence thesis;

    end;

    scheme :: BINOP_2:sch21

    ILambdaD { F( Integer) -> Integer } :

ex f be Function of INT , INT st for x be Integer holds (f . x) = F(x);

      defpred P[ Element of INT , set] means $2 = F($1);

      

       A1: for x be Element of INT holds ex y be Element of INT st P[x, y]

      proof

        let x be Element of INT ;

        reconsider y = F(x) as Element of INT by INT_1:def 2;

        take y;

        thus P[x, y];

      end;

      consider f be Function of INT , INT such that

       A2: for x be Element of INT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      let c be Integer;

      reconsider c as Element of INT by INT_1:def 2;

       P[c, (f . c)] by A2;

      hence thesis;

    end;

    scheme :: BINOP_2:sch22

    NLambdaD { F( Nat) -> Nat } :

ex f be sequence of NAT st for x be Nat holds (f . x) = F(x);

      defpred P[ Element of NAT , set] means $2 = F($1);

      

       A1: for x be Element of NAT holds ex y be Element of NAT st P[x, y]

      proof

        let x be Element of NAT ;

        reconsider y = F(x) as Element of NAT by ORDINAL1:def 12;

        take y;

        thus P[x, y];

      end;

      consider f be sequence of NAT such that

       A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      let c be Nat;

      reconsider c as Element of NAT by ORDINAL1:def 12;

       P[c, (f . c)] by A2;

      hence thesis;

    end;

    reserve c,c1,c2 for Complex;

    reserve r,r1,r2 for Real;

    reserve w,w1,w2 for Rational;

    reserve i,i1,i2 for Integer;

    reserve n1,n2 for Nat;

    definition

      :: BINOP_2:def1

      func compcomplex -> UnOp of COMPLEX means for c holds (it . c) = ( - c);

      existence from CLambdaD;

      uniqueness from CFuncDefUniq;

      :: BINOP_2:def2

      func invcomplex -> UnOp of COMPLEX means for c holds (it . c) = (c " );

      existence from CLambdaD;

      uniqueness from CFuncDefUniq;

      :: BINOP_2:def3

      func addcomplex -> BinOp of COMPLEX means

      : Def3: for c1, c2 holds (it . (c1,c2)) = (c1 + c2);

      existence from CLambda2D;

      uniqueness from CBinOpDefuniq;

      :: BINOP_2:def4

      func diffcomplex -> BinOp of COMPLEX means for c1, c2 holds (it . (c1,c2)) = (c1 - c2);

      existence from CLambda2D;

      uniqueness from CBinOpDefuniq;

      :: BINOP_2:def5

      func multcomplex -> BinOp of COMPLEX means

      : Def5: for c1, c2 holds (it . (c1,c2)) = (c1 * c2);

      existence from CLambda2D;

      uniqueness from CBinOpDefuniq;

      :: BINOP_2:def6

      func divcomplex -> BinOp of COMPLEX means for c1, c2 holds (it . (c1,c2)) = (c1 / c2);

      existence from CLambda2D;

      uniqueness from CBinOpDefuniq;

    end

    definition

      :: BINOP_2:def7

      func compreal -> UnOp of REAL means for r holds (it . r) = ( - r);

      existence from RLambdaD;

      uniqueness from RFuncDefUniq;

      :: BINOP_2:def8

      func invreal -> UnOp of REAL means for r holds (it . r) = (r " );

      existence from RLambdaD;

      uniqueness from RFuncDefUniq;

      :: BINOP_2:def9

      func addreal -> BinOp of REAL means

      : Def9: for r1, r2 holds (it . (r1,r2)) = (r1 + r2);

      existence from RLambda2D;

      uniqueness from RBinOpDefuniq;

      :: BINOP_2:def10

      func diffreal -> BinOp of REAL means for r1, r2 holds (it . (r1,r2)) = (r1 - r2);

      existence from RLambda2D;

      uniqueness from RBinOpDefuniq;

      :: BINOP_2:def11

      func multreal -> BinOp of REAL means

      : Def11: for r1, r2 holds (it . (r1,r2)) = (r1 * r2);

      existence from RLambda2D;

      uniqueness from RBinOpDefuniq;

      :: BINOP_2:def12

      func divreal -> BinOp of REAL means for r1, r2 holds (it . (r1,r2)) = (r1 / r2);

      existence from RLambda2D;

      uniqueness from RBinOpDefuniq;

    end

    definition

      :: BINOP_2:def13

      func comprat -> UnOp of RAT means for w holds (it . w) = ( - w);

      existence from WLambdaD;

      uniqueness from WFuncDefUniq;

      :: BINOP_2:def14

      func invrat -> UnOp of RAT means for w holds (it . w) = (w " );

      existence from WLambdaD;

      uniqueness from WFuncDefUniq;

      :: BINOP_2:def15

      func addrat -> BinOp of RAT means

      : Def15: for w1, w2 holds (it . (w1,w2)) = (w1 + w2);

      existence from WLambda2D;

      uniqueness from WBinOpDefuniq;

      :: BINOP_2:def16

      func diffrat -> BinOp of RAT means for w1, w2 holds (it . (w1,w2)) = (w1 - w2);

      existence from WLambda2D;

      uniqueness from WBinOpDefuniq;

      :: BINOP_2:def17

      func multrat -> BinOp of RAT means

      : Def17: for w1, w2 holds (it . (w1,w2)) = (w1 * w2);

      existence from WLambda2D;

      uniqueness from WBinOpDefuniq;

      :: BINOP_2:def18

      func divrat -> BinOp of RAT means for w1, w2 holds (it . (w1,w2)) = (w1 / w2);

      existence from WLambda2D;

      uniqueness from WBinOpDefuniq;

    end

    definition

      :: BINOP_2:def19

      func compint -> UnOp of INT means for i holds (it . i) = ( - i);

      existence from ILambdaD;

      uniqueness from IFuncDefUniq;

      :: BINOP_2:def20

      func addint -> BinOp of INT means

      : Def20: for i1, i2 holds (it . (i1,i2)) = (i1 + i2);

      existence from ILambda2D;

      uniqueness from IBinOpDefuniq;

      :: BINOP_2:def21

      func diffint -> BinOp of INT means for i1, i2 holds (it . (i1,i2)) = (i1 - i2);

      existence from ILambda2D;

      uniqueness from IBinOpDefuniq;

      :: BINOP_2:def22

      func multint -> BinOp of INT means

      : Def22: for i1, i2 holds (it . (i1,i2)) = (i1 * i2);

      existence from ILambda2D;

      uniqueness from IBinOpDefuniq;

    end

    definition

      :: BINOP_2:def23

      func addnat -> BinOp of NAT means

      : Def23: for n1, n2 holds (it . (n1,n2)) = (n1 + n2);

      existence from NLambda2D;

      uniqueness from NBinOpDefuniq;

      :: BINOP_2:def24

      func multnat -> BinOp of NAT means

      : Def24: for n1, n2 holds (it . (n1,n2)) = (n1 * n2);

      existence from NLambda2D;

      uniqueness from NBinOpDefuniq;

    end

    registration

      cluster addcomplex -> commutative associative;

      coherence

      proof

        thus addcomplex is commutative

        proof

          let c1,c2 be Element of COMPLEX ;

          

          thus ( addcomplex . (c1,c2)) = (c1 + c2) by Def3

          .= ( addcomplex . (c2,c1)) by Def3;

        end;

        let c1,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

      proof

        thus multcomplex is commutative

        proof

          let c1,c2 be Element of COMPLEX ;

          

          thus ( multcomplex . (c1,c2)) = (c1 * c2) by Def5

          .= ( multcomplex . (c2,c1)) by Def5;

        end;

        let c1,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

      proof

        thus addreal is commutative

        proof

          let r1,r2 be Element of REAL ;

          

          thus ( addreal . (r1,r2)) = (r1 + r2) by Def9

          .= ( addreal . (r2,r1)) by Def9;

        end;

        let r1,r2,r3 be Element of REAL ;

        

        thus ( addreal . (r1,( addreal . (r2,r3)))) = (r1 + ( addreal . (r2,r3))) by Def9

        .= (r1 + (r2 + r3)) by Def9

        .= ((r1 + r2) + r3)

        .= (( addreal . (r1,r2)) + r3) by Def9

        .= ( addreal . (( addreal . (r1,r2)),r3)) by Def9;

      end;

      cluster multreal -> commutative associative;

      coherence

      proof

        thus multreal is commutative

        proof

          let r1,r2 be Element of REAL ;

          

          thus ( multreal . (r1,r2)) = (r1 * r2) by Def11

          .= ( multreal . (r2,r1)) by Def11;

        end;

        let r1,r2,r3 be Element of REAL ;

        

        thus ( multreal . (r1,( multreal . (r2,r3)))) = (r1 * ( multreal . (r2,r3))) by Def11

        .= (r1 * (r2 * r3)) by Def11

        .= ((r1 * r2) * r3)

        .= (( multreal . (r1,r2)) * r3) by Def11

        .= ( multreal . (( multreal . (r1,r2)),r3)) by Def11;

      end;

      cluster addrat -> commutative associative;

      coherence

      proof

        thus addrat is commutative

        proof

          let w1,w2 be Element of RAT ;

          

          thus ( addrat . (w1,w2)) = (w1 + w2) by Def15

          .= ( addrat . (w2,w1)) by Def15;

        end;

        let w1,w2,w3 be Element of RAT ;

        

        thus ( addrat . (w1,( addrat . (w2,w3)))) = (w1 + ( addrat . (w2,w3))) by Def15

        .= (w1 + (w2 + w3)) by Def15

        .= ((w1 + w2) + w3)

        .= (( addrat . (w1,w2)) + w3) by Def15

        .= ( addrat . (( addrat . (w1,w2)),w3)) by Def15;

      end;

      cluster multrat -> commutative associative;

      coherence

      proof

        thus multrat is commutative

        proof

          let w1,w2 be Element of RAT ;

          

          thus ( multrat . (w1,w2)) = (w1 * w2) by Def17

          .= ( multrat . (w2,w1)) by Def17;

        end;

        let w1,w2,w3 be Element of RAT ;

        

        thus ( multrat . (w1,( multrat . (w2,w3)))) = (w1 * ( multrat . (w2,w3))) by Def17

        .= (w1 * (w2 * w3)) by Def17

        .= ((w1 * w2) * w3)

        .= (( multrat . (w1,w2)) * w3) by Def17

        .= ( multrat . (( multrat . (w1,w2)),w3)) by Def17;

      end;

      cluster addint -> commutative associative;

      coherence

      proof

        thus addint is commutative

        proof

          let i1,i2 be Element of INT ;

          

          thus ( addint . (i1,i2)) = (i1 + i2) by Def20

          .= ( addint . (i2,i1)) by Def20;

        end;

        let i1,i2,i3 be Element of INT ;

        

        thus ( addint . (i1,( addint . (i2,i3)))) = (i1 + ( addint . (i2,i3))) by Def20

        .= (i1 + (i2 + i3)) by Def20

        .= ((i1 + i2) + i3)

        .= (( addint . (i1,i2)) + i3) by Def20

        .= ( addint . (( addint . (i1,i2)),i3)) by Def20;

      end;

      cluster multint -> commutative associative;

      coherence

      proof

        thus multint is commutative

        proof

          let i1,i2 be Element of INT ;

          

          thus ( multint . (i1,i2)) = (i1 * i2) by Def22

          .= ( multint . (i2,i1)) by Def22;

        end;

        let i1,i2,i3 be Element of INT ;

        

        thus ( multint . (i1,( multint . (i2,i3)))) = (i1 * ( multint . (i2,i3))) by Def22

        .= (i1 * (i2 * i3)) by Def22

        .= ((i1 * i2) * i3)

        .= (( multint . (i1,i2)) * i3) by Def22

        .= ( multint . (( multint . (i1,i2)),i3)) by Def22;

      end;

      cluster addnat -> commutative associative;

      coherence

      proof

        thus addnat is commutative

        proof

          let n1,n2 be Element of NAT ;

          

          thus ( addnat . (n1,n2)) = (n1 + n2) by Def23

          .= ( addnat . (n2,n1)) by Def23;

        end;

        let n1,n2,n3 be Element of NAT ;

        

        thus ( addnat . (n1,( addnat . (n2,n3)))) = (n1 + ( addnat . (n2,n3))) by Def23

        .= (n1 + (n2 + n3)) by Def23

        .= ((n1 + n2) + n3)

        .= (( addnat . (n1,n2)) + n3) by Def23

        .= ( addnat . (( addnat . (n1,n2)),n3)) by Def23;

      end;

      cluster multnat -> commutative associative;

      coherence

      proof

        thus multnat is commutative

        proof

          let n1,n2 be Element of NAT ;

          

          thus ( multnat . (n1,n2)) = (n1 * n2) by Def24

          .= ( multnat . (n2,n1)) by Def24;

        end;

        let n1,n2,n3 be Element of NAT ;

        

        thus ( multnat . (n1,( multnat . (n2,n3)))) = (n1 * ( multnat . (n2,n3))) by Def24

        .= (n1 * (n2 * n3)) by Def24

        .= ((n1 * n2) * n3)

        .= (( multnat . (n1,n2)) * n3) by Def24

        .= ( multnat . (( multnat . (n1,n2)),n3)) by Def24;

      end;

    end

    

     Lm1: 0 in NAT ;

    

     Lm2: 0 is_a_unity_wrt addcomplex

    proof

      thus for c be Element of COMPLEX holds ( addcomplex . ( 0 ,c)) = c

      proof

        let c be Element of COMPLEX ;

        

        thus ( addcomplex . ( 0 ,c)) = ( 0 + c) by Def3

        .= c;

      end;

      let c be Element of COMPLEX ;

      

      thus ( addcomplex . (c, 0 )) = (c + 0 ) by Def3

      .= c;

    end;

    

     Lm3: ( In ( 0 , REAL )) is_a_unity_wrt addreal

    proof

      thus for r be Element of REAL holds ( addreal . (( In ( 0 , REAL )),r)) = r

      proof

        let r be Element of REAL ;

        

        thus ( addreal . (( In ( 0 , REAL )),r)) = ( 0 + r) by Def9

        .= r;

      end;

      let r be Element of REAL ;

      

      thus ( addreal . (r,( In ( 0 , REAL )))) = (r + 0 ) by Def9

      .= r;

    end;

    

     Lm4: 0 is_a_unity_wrt addrat

    proof

      thus for w be Element of RAT holds ( addrat . ( 0 ,w)) = w

      proof

        let w be Element of RAT ;

        

        thus ( addrat . ( 0 ,w)) = ( 0 + w) by Def15

        .= w;

      end;

      let w be Element of RAT ;

      

      thus ( addrat . (w, 0 )) = (w + 0 ) by Def15

      .= w;

    end;

    

     Lm5: 0 is_a_unity_wrt addint

    proof

      thus for i be Element of INT holds ( addint . ( 0 ,i)) = i

      proof

        let i be Element of INT ;

        

        thus ( addint . ( 0 ,i)) = ( 0 + i) by Def20

        .= i;

      end;

      let i be Element of INT ;

      

      thus ( addint . (i, 0 )) = (i + 0 ) by Def20

      .= i;

    end;

    

     Lm6: 0 is_a_unity_wrt addnat

    proof

      thus for n be Element of NAT holds ( addnat . ( 0 ,n)) = n

      proof

        let n be Element of NAT ;

        

        thus ( addnat . ( 0 ,n)) = ( 0 + n) by Def23

        .= n;

      end;

      let n be Element of NAT ;

      

      thus ( addnat . (n, 0 )) = (n + 0 ) by Def23

      .= n;

    end;

    

     Lm7: 1 in NAT ;

    

     Lm8: 1 is_a_unity_wrt multcomplex

    proof

      thus for c be Element of COMPLEX holds ( multcomplex . (1,c)) = c

      proof

        let c be Element of COMPLEX ;

        

        thus ( multcomplex . (1,c)) = (1 * c) by Def5

        .= c;

      end;

      let c be Element of COMPLEX ;

      

      thus ( multcomplex . (c,1)) = (c * 1) by Def5

      .= c;

    end;

    

     Lm9: 1 is_a_unity_wrt multreal

    proof

      1 in NAT ;

      then

      reconsider j = 1 as Element of REAL by NUMBERS: 19;

      thus for r be Element of REAL holds ( multreal . (1,r)) = r

      proof

        let r be Element of REAL ;

        

        thus ( multreal . (1,r)) = (1 * r) by Def11

        .= r;

      end;

      let r be Element of REAL ;

      

      thus ( multreal . (r,1)) = (r * 1) by Def11

      .= r;

    end;

    

     Lm10: 1 is_a_unity_wrt multrat

    proof

      thus for w be Element of RAT holds ( multrat . (1,w)) = w

      proof

        let w be Element of RAT ;

        

        thus ( multrat . (1,w)) = (1 * w) by Def17

        .= w;

      end;

      let w be Element of RAT ;

      

      thus ( multrat . (w,1)) = (w * 1) by Def17

      .= w;

    end;

    

     Lm11: 1 is_a_unity_wrt multint

    proof

      thus for i be Element of INT holds ( multint . (1,i)) = i

      proof

        let i be Element of INT ;

        

        thus ( multint . (1,i)) = (1 * i) by Def22

        .= i;

      end;

      let i be Element of INT ;

      

      thus ( multint . (i,1)) = (i * 1) by Def22

      .= i;

    end;

    

     Lm12: 1 is_a_unity_wrt multnat

    proof

      thus for n be Element of NAT holds ( multnat . (1,n)) = n

      proof

        let n be Element of NAT ;

        

        thus ( multnat . (1,n)) = (1 * n) by Def24

        .= n;

      end;

      let n be Element of NAT ;

      

      thus ( multnat . (n,1)) = (n * 1) by Def24

      .= n;

    end;

    registration

      cluster addcomplex -> having_a_unity;

      coherence by Lm1, NUMBERS: 20, Lm2, SETWISEO:def 2;

      cluster addreal -> having_a_unity;

      coherence by Lm3, SETWISEO:def 2;

      cluster addrat -> having_a_unity;

      coherence by Lm1, NUMBERS: 18, Lm4, SETWISEO:def 2;

      cluster addint -> having_a_unity;

      coherence by Lm1, NUMBERS: 17, Lm5, SETWISEO:def 2;

      cluster addnat -> having_a_unity;

      coherence by Lm6, SETWISEO:def 2;

      cluster multcomplex -> having_a_unity;

      coherence by Lm7, NUMBERS: 20, Lm8, SETWISEO:def 2;

      cluster multreal -> having_a_unity;

      coherence by Lm7, NUMBERS: 19, Lm9, SETWISEO:def 2;

      cluster multrat -> having_a_unity;

      coherence by Lm7, NUMBERS: 18, Lm10, SETWISEO:def 2;

      cluster multint -> having_a_unity;

      coherence by Lm7, NUMBERS: 17, Lm11, SETWISEO:def 2;

      cluster multnat -> having_a_unity;

      coherence by Lm12, SETWISEO:def 2;

    end

    theorem :: BINOP_2:1

    ( the_unity_wrt addcomplex ) = 0 by Lm1, NUMBERS: 20, Lm2, BINOP_1:def 8;

    theorem :: BINOP_2:2

    ( the_unity_wrt addreal ) = 0 by Lm3, BINOP_1:def 8;

    theorem :: BINOP_2:3

    ( the_unity_wrt addrat ) = 0 by Lm1, NUMBERS: 18, Lm4, BINOP_1:def 8;

    theorem :: BINOP_2:4

    ( the_unity_wrt addint ) = 0 by Lm1, NUMBERS: 17, Lm5, BINOP_1:def 8;

    theorem :: BINOP_2:5

    ( the_unity_wrt addnat ) = 0 by Lm6, BINOP_1:def 8;

    theorem :: BINOP_2:6

    ( the_unity_wrt multcomplex ) = 1 by Lm7, NUMBERS: 20, Lm8, BINOP_1:def 8;

    theorem :: BINOP_2:7

    ( the_unity_wrt multreal ) = 1 by Lm7, NUMBERS: 19, Lm9, BINOP_1:def 8;

    theorem :: BINOP_2:8

    ( the_unity_wrt multrat ) = 1 by Lm7, NUMBERS: 18, Lm10, BINOP_1:def 8;

    theorem :: BINOP_2:9

    ( the_unity_wrt multint ) = 1 by Lm7, NUMBERS: 17, Lm11, BINOP_1:def 8;

    theorem :: BINOP_2:10

    ( the_unity_wrt multnat ) = 1 by Lm12, BINOP_1:def 8;

    registration

      let f be real-valued Function;

      let a,b be object;

      cluster (f . (a,b)) -> real;

      coherence ;

    end