algstr_1.miz



    begin

    reserve L for non empty addLoopStr;

    reserve a,b,c,x for Element of L;

    theorem :: ALGSTR_1:1

    

     Th1: (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) implies ((a + b) = ( 0. L) implies (b + a) = ( 0. L))

    proof

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c));

      consider x such that

       A4: (b + x) = ( 0. L) by A2;

      assume

       A5: (a + b) = ( 0. L);

      

      thus (b + a) = ((b + a) + (b + x)) by A1, A4

      .= (((b + a) + b) + x) by A3

      .= ((b + ( 0. L)) + x) by A3, A5

      .= ( 0. L) by A1, A4;

    end;

    theorem :: ALGSTR_1:2

    (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) implies (( 0. L) + a) = (a + ( 0. L))

    proof

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c));

      consider x such that

       A4: (a + x) = ( 0. L) by A2;

      

      thus (( 0. L) + a) = (a + (x + a)) by A3, A4

      .= (a + ( 0. L)) by A1, A2, A3, A4, Th1;

    end;

    theorem :: ALGSTR_1:3

    (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) implies for a holds ex x st (x + a) = ( 0. L)

    proof

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c));

      let a;

      consider x such that

       A4: (a + x) = ( 0. L) by A2;

      (x + a) = ( 0. L) by A1, A2, A3, A4, Th1;

      hence thesis;

    end;

    definition

      let x be set;

      :: ALGSTR_1:def1

      func Extract x -> Element of {x} equals x;

      coherence by TARSKI:def 1;

    end

    theorem :: ALGSTR_1:4

    

     Th4: for a,b be Element of Trivial-addLoopStr holds a = b

    proof

      let a,b be Element of Trivial-addLoopStr ;

      

      thus a = {} by TARSKI:def 1

      .= b by TARSKI:def 1;

    end;

    theorem :: ALGSTR_1:5

    for a,b be Element of Trivial-addLoopStr holds (a + b) = ( 0. Trivial-addLoopStr ) by Th4;

    

     Lm1: (for a be Element of Trivial-addLoopStr holds (a + ( 0. Trivial-addLoopStr )) = a) & for a be Element of Trivial-addLoopStr holds (( 0. Trivial-addLoopStr ) + a) = a by Th4;

    

     Lm2: for a,b be Element of Trivial-addLoopStr holds ex x be Element of Trivial-addLoopStr st (a + x) = b

    proof

      let a,b be Element of Trivial-addLoopStr ;

      take ( 0. Trivial-addLoopStr );

      thus thesis by Th4;

    end;

    

     Lm3: for a,b be Element of Trivial-addLoopStr holds ex x be Element of Trivial-addLoopStr st (x + a) = b

    proof

      let a,b be Element of Trivial-addLoopStr ;

      take ( 0. Trivial-addLoopStr );

      thus thesis by Th4;

    end;

    

     Lm4: (for a,x,y be Element of Trivial-addLoopStr holds (a + x) = (a + y) implies x = y) & for a,x,y be Element of Trivial-addLoopStr holds (x + a) = (y + a) implies x = y by Th4;

    definition

      let IT be non empty addLoopStr;

      :: ALGSTR_1:def2

      attr IT is left_zeroed means for a be Element of IT holds (( 0. IT) + a) = a;

    end

    definition

      let L be non empty addLoopStr;

      :: ALGSTR_1:def3

      attr L is add-left-invertible means

      : Def3: for a,b be Element of L holds ex x be Element of L st (x + a) = b;

      :: ALGSTR_1:def4

      attr L is add-right-invertible means

      : Def4: for a,b be Element of L holds ex x be Element of L st (a + x) = b;

    end

    definition

      let IT be non empty addLoopStr;

      :: ALGSTR_1:def5

      attr IT is Loop-like means IT is left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible;

    end

    registration

      cluster Loop-like -> left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible for non empty addLoopStr;

      coherence ;

      cluster left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible -> Loop-like for non empty addLoopStr;

      coherence ;

    end

    theorem :: ALGSTR_1:6

    

     Th6: for L be non empty addLoopStr holds L is Loop-like iff (for a,b be Element of L holds ex x be Element of L st (a + x) = b) & (for a,b be Element of L holds ex x be Element of L st (x + a) = b) & (for a,x,y be Element of L holds (a + x) = (a + y) implies x = y) & for a,x,y be Element of L holds (x + a) = (y + a) implies x = y

    proof

      let L be non empty addLoopStr;

      thus L is Loop-like implies (for a,b be Element of L holds ex x be Element of L st (a + x) = b) & (for a,b be Element of L holds ex x be Element of L st (x + a) = b) & (for a,x,y be Element of L holds (a + x) = (a + y) implies x = y) & for a,x,y be Element of L st (x + a) = (y + a) holds x = y by Def3, Def4, ALGSTR_0:def 3, ALGSTR_0:def 4;

      assume that

       A1: (for a,b be Element of L holds ex x be Element of L st (a + x) = b) & for a,b be Element of L holds ex x be Element of L st (x + a) = b and

       A2: for a,x,y be Element of L holds (a + x) = (a + y) implies x = y and

       A3: for a,x,y be Element of L holds (x + a) = (y + a) implies x = y;

      thus L is left_add-cancelable

      proof

        let x,x,x be Element of L;

        thus thesis by A2;

      end;

      thus L is right_add-cancelable

      proof

        let x,x,x be Element of L;

        thus thesis by A3;

      end;

      thus thesis by A1;

    end;

    

     Lm5: for a,b,c be Element of Trivial-addLoopStr holds ((a + b) + c) = (a + (b + c)) by Th4;

    

     Lm6: for a,b be Element of Trivial-addLoopStr holds (a + b) = (b + a) by Th4;

    registration

      cluster Trivial-addLoopStr -> add-associative Loop-like right_zeroed left_zeroed;

      coherence by Lm1, Lm2, Lm3, Lm4, Lm5, Th6;

    end

    registration

      cluster strict left_zeroed right_zeroed Loop-like for non empty addLoopStr;

      existence

      proof

        take Trivial-addLoopStr ;

        thus thesis;

      end;

    end

    definition

      mode Loop is left_zeroed right_zeroed Loop-like non empty addLoopStr;

    end

    registration

      cluster strict add-associative for Loop;

      existence

      proof

        take Trivial-addLoopStr ;

        thus thesis;

      end;

    end

    registration

      cluster Loop-like -> add-left-invertible for non empty addLoopStr;

      coherence ;

      cluster add-associative right_zeroed right_complementable -> left_zeroed Loop-like for non empty addLoopStr;

      coherence

      proof

        let L;

        assume

         A1: L is add-associative right_zeroed right_complementable;

        then

        reconsider G = L as add-associative right_zeroed right_complementable non empty addLoopStr;

        

         A2: for a,x,y be Element of L holds (x + a) = (y + a) implies x = y by A1, RLVECT_1: 8;

        thus for a holds (( 0. L) + a) = a by A1, RLVECT_1: 4;

        

         A3: for a, b holds ex x st (x + a) = b

        proof

          let a, b;

          reconsider a9 = a, b9 = b as Element of G;

          reconsider x = (b9 + ( - a9)) as Element of L;

          take x;

          ((b9 + ( - a9)) + a9) = (b9 + (( - a9) + a9)) by RLVECT_1:def 3

          .= (b9 + ( 0. G)) by RLVECT_1: 5

          .= b by RLVECT_1: 4;

          hence thesis;

        end;

        (for a, b holds ex x st (a + x) = b) & for a,x,y be Element of L holds (a + x) = (a + y) implies x = y by A1, RLVECT_1: 7, RLVECT_1: 8;

        hence thesis by A3, A2, Th6;

      end;

    end

    theorem :: ALGSTR_1:7

    

     Th7: L is AddGroup iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & for a, b, c holds ((a + b) + c) = (a + (b + c))

    proof

      thus L is AddGroup implies (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & for a, b, c holds ((a + b) + c) = (a + (b + c)) by Th6, RLVECT_1:def 3, RLVECT_1:def 4;

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c));

      L is right_complementable

      proof

        let a be Element of L;

        thus ex x st (a + x) = ( 0. L) by A2;

      end;

      hence thesis by A1, A3, RLVECT_1:def 3, RLVECT_1:def 4;

    end;

    registration

      cluster Trivial-addLoopStr -> Abelian;

      coherence by Lm6;

    end

    registration

      cluster strict Abelian for AddGroup;

      existence

      proof

        take Trivial-addLoopStr ;

        thus thesis;

      end;

    end

    theorem :: ALGSTR_1:8

    L is Abelian AddGroup iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & for a, b holds (a + b) = (b + a) by Th7, RLVECT_1:def 2;

    registration

      cluster Trivial-multLoopStr -> non empty;

      coherence ;

    end

    theorem :: ALGSTR_1:9

    

     Th9: for a,b be Element of Trivial-multLoopStr holds a = b

    proof

      let a,b be Element of Trivial-multLoopStr ;

      

      thus a = {} by TARSKI:def 1

      .= b by TARSKI:def 1;

    end;

    theorem :: ALGSTR_1:10

    for a,b be Element of Trivial-multLoopStr holds (a * b) = ( 1. Trivial-multLoopStr ) by Th9;

    

     Lm7: (for a be Element of Trivial-multLoopStr holds (a * ( 1. Trivial-multLoopStr )) = a) & for a be Element of Trivial-multLoopStr holds (( 1. Trivial-multLoopStr ) * a) = a by Th9;

    

     Lm8: for a,b be Element of Trivial-multLoopStr holds ex x be Element of Trivial-multLoopStr st (a * x) = b

    proof

      let a,b be Element of Trivial-multLoopStr ;

      take ( 1_ Trivial-multLoopStr );

      thus thesis by Th9;

    end;

    

     Lm9: for a,b be Element of Trivial-multLoopStr holds ex x be Element of Trivial-multLoopStr st (x * a) = b

    proof

      let a,b be Element of Trivial-multLoopStr ;

      take ( 1_ Trivial-multLoopStr );

      thus thesis by Th9;

    end;

    definition

      let IT be non empty multLoopStr;

      :: ALGSTR_1:def6

      attr IT is invertible means

      : Def6: (for a,b be Element of IT holds ex x be Element of IT st (a * x) = b) & for a,b be Element of IT holds ex x be Element of IT st (x * a) = b;

    end

    notation

      let L be non empty multLoopStr;

      synonym L is cancelable for L is mult-cancelable;

    end

    registration

      cluster strict well-unital invertible cancelable for non empty multLoopStr;

      existence

      proof

         Trivial-multLoopStr is well-unital invertible cancelable by Lm7, Lm8, Lm9;

        hence thesis;

      end;

    end

    definition

      mode multLoop is well-unital invertible cancelable non empty multLoopStr;

    end

    registration

      cluster Trivial-multLoopStr -> well-unital invertible cancelable;

      coherence by Lm7, Lm8, Lm9;

    end

    

     Lm10: for a,b,c be Element of Trivial-multLoopStr holds ((a * b) * c) = (a * (b * c)) by Th9;

    registration

      cluster strict associative for multLoop;

      existence

      proof

         Trivial-multLoopStr is associative by Lm10;

        hence thesis;

      end;

    end

    definition

      mode multGroup is associative multLoop;

    end

    reserve L for non empty multLoopStr;

    reserve a,b,c,x,y,z for Element of L;

    

     Lm11: (for a holds (a * ( 1. L)) = a) & (for a holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) implies ((a * b) = ( 1. L) implies (b * a) = ( 1. L))

    proof

      assume that

       A1: for a holds (a * ( 1. L)) = a and

       A2: for a holds ex x st (a * x) = ( 1. L) and

       A3: for a, b, c holds ((a * b) * c) = (a * (b * c));

      consider x such that

       A4: (b * x) = ( 1. L) by A2;

      assume

       A5: (a * b) = ( 1. L);

      

      thus (b * a) = ((b * a) * (b * x)) by A1, A4

      .= (((b * a) * b) * x) by A3

      .= ((b * ( 1. L)) * x) by A3, A5

      .= ( 1. L) by A1, A4;

    end;

    

     Lm12: (for a holds (a * ( 1. L)) = a) & (for a holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) implies (( 1. L) * a) = (a * ( 1. L))

    proof

      assume that

       A1: for a holds (a * ( 1. L)) = a and

       A2: for a holds ex x st (a * x) = ( 1. L) and

       A3: for a, b, c holds ((a * b) * c) = (a * (b * c));

      consider x such that

       A4: (a * x) = ( 1. L) by A2;

      

      thus (( 1. L) * a) = (a * (x * a)) by A3, A4

      .= (a * ( 1. L)) by A1, A2, A3, A4, Lm11;

    end;

    

     Lm13: (for a holds (a * ( 1. L)) = a) & (for a holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) implies for a holds ex x st (x * a) = ( 1. L)

    proof

      assume that

       A1: for a holds (a * ( 1. L)) = a and

       A2: for a holds ex x st (a * x) = ( 1. L) and

       A3: for a, b, c holds ((a * b) * c) = (a * (b * c));

      let a;

      consider x such that

       A4: (a * x) = ( 1. L) by A2;

      (x * a) = ( 1. L) by A1, A2, A3, A4, Lm11;

      hence thesis;

    end;

    theorem :: ALGSTR_1:11

    

     Th11: L is multGroup iff (for a holds (a * ( 1. L)) = a) & (for a holds ex x st (a * x) = ( 1. L)) & for a, b, c holds ((a * b) * c) = (a * (b * c))

    proof

      thus L is multGroup implies (for a holds (a * ( 1. L)) = a) & (for a holds ex x st (a * x) = ( 1. L)) & for a, b, c holds ((a * b) * c) = (a * (b * c)) by Def6, GROUP_1:def 3;

      assume that

       A1: for a holds (a * ( 1. L)) = a and

       A2: for a holds ex x st (a * x) = ( 1. L) and

       A3: for a, b, c holds ((a * b) * c) = (a * (b * c));

      

       A4: for a,b be Element of L holds ex x be Element of L st (x * a) = b

      proof

        let a, b;

        consider y such that

         A5: (y * a) = ( 1. L) by A1, A2, A3, Lm13;

        take x = (b * y);

        

        thus (x * a) = (b * ( 1. L)) by A3, A5

        .= b by A1;

      end;

      

       A6: for a be Element of L holds (( 1. L) * a) = a

      proof

        let a;

        

        thus (( 1. L) * a) = (a * ( 1. L)) by A1, A2, A3, Lm12

        .= a by A1;

      end;

      

       A7: L is left_mult-cancelable

      proof

        let a, x, y;

        consider z such that

         A8: (z * a) = ( 1. L) by A1, A2, A3, Lm13;

        assume (a * x) = (a * y);

        

        then ((z * a) * x) = (z * (a * y)) by A3

        .= ((z * a) * y) by A3;

        

        hence x = (( 1. L) * y) by A6, A8

        .= y by A6;

      end;

      

       A9: L is right_mult-cancelable

      proof

        let a, x, y;

        consider z such that

         A10: (a * z) = ( 1. L) by A2;

        assume (x * a) = (y * a);

        

        then (x * (a * z)) = ((y * a) * z) by A3

        .= (y * (a * z)) by A3;

        

        hence x = (y * ( 1. L)) by A1, A10

        .= y by A1;

      end;

      for a,b be Element of L holds ex x be Element of L st (a * x) = b

      proof

        let a, b;

        consider y such that

         A11: (a * y) = ( 1. L) by A2;

        take x = (y * b);

        

        thus (a * x) = (( 1. L) * b) by A3, A11

        .= b by A6;

      end;

      hence thesis by A1, A3, A6, A4, A7, A9, Def6, GROUP_1:def 3, VECTSP_1:def 6;

    end;

    registration

      cluster Trivial-multLoopStr -> associative;

      coherence by Lm10;

    end

    

     Lm14: for a,b be Element of Trivial-multLoopStr holds (a * b) = (b * a) by Th9;

    registration

      cluster strict commutative for multGroup;

      existence

      proof

         Trivial-multLoopStr is commutative by Lm14;

        hence thesis;

      end;

    end

    theorem :: ALGSTR_1:12

    L is commutative multGroup iff (for a holds (a * ( 1. L)) = a) & (for a holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & for a, b holds (a * b) = (b * a) by Th11, GROUP_1:def 12;

    notation

      let L be invertible cancelable non empty multLoopStr;

      let x be Element of L;

      synonym x " for / x;

    end

    registration

      let L be invertible cancelable non empty multLoopStr;

      cluster -> left_invertible for Element of L;

      coherence by Def6;

    end

    reserve G for multGroup;

    reserve a,b,c,x for Element of G;

    theorem :: ALGSTR_1:13

    ((a " ) * a) = ( 1. G) & (a * (a " )) = ( 1. G)

    proof

      thus

       A1: ((a " ) * a) = ( 1. G) by ALGSTR_0:def 30;

      

       A2: for a, b, c holds ((a * b) * c) = (a * (b * c)) by Th11;

      (for a holds (a * ( 1. G)) = a) & for a holds ex x st (a * x) = ( 1. G) by Th11;

      hence thesis by A1, A2, Lm11;

    end;

    ::$Canceled

    definition

      :: ALGSTR_1:def7

      func multEX_0 -> strict multLoopStr_0 equals multLoopStr_0 (# REAL , multreal , ( In ( 0 , REAL )), ( In (1, REAL )) #);

      correctness ;

    end

    registration

      cluster multEX_0 -> non empty;

      coherence ;

    end

     Lm15:

    now

      let x,e be Element of multEX_0 ;

      reconsider a = x as Real;

      assume

       A1: e = 1;

      

      hence (x * e) = (a * 1) by BINOP_2:def 11

      .= x;

      

      thus (e * x) = (1 * a) by A1, BINOP_2:def 11

      .= x;

    end;

    registration

      cluster multEX_0 -> well-unital;

      coherence by Lm15;

    end

    

     Lm16: for a,b be Element of multEX_0 st a <> ( 0. multEX_0 ) holds ex x be Element of multEX_0 st (a * x) = b

    proof

      let a,b be Element of multEX_0 such that

       A1: a <> ( 0. multEX_0 );

      reconsider p = a, q = b as Element of REAL ;

      reconsider x = (q / p) as Element of multEX_0 ;

      (p * (q / p)) = q by A1, XCMPLX_1: 87;

      then (a * x) = b by BINOP_2:def 11;

      hence thesis;

    end;

    

     Lm17: for a,b be Element of multEX_0 st a <> ( 0. multEX_0 ) holds ex x be Element of multEX_0 st (x * a) = b

    proof

      let a,b be Element of multEX_0 such that

       A1: a <> ( 0. multEX_0 );

      reconsider p = a, q = b as Element of REAL ;

      reconsider x = (q / p) as Element of multEX_0 ;

      (p * (q / p)) = q by A1, XCMPLX_1: 87;

      then (x * a) = b by BINOP_2:def 11;

      hence thesis;

    end;

    

     Lm18: for a,x,y be Element of multEX_0 st a <> ( 0. multEX_0 ) holds (a * x) = (a * y) implies x = y

    proof

      let a,x,y be Element of multEX_0 such that

       A1: a <> ( 0. multEX_0 );

      reconsider aa = a, p = x, q = y as Real;

      assume (a * x) = (a * y);

      

      then (aa * p) = (a * y) by BINOP_2:def 11

      .= (aa * q) by BINOP_2:def 11;

      hence thesis by A1, XCMPLX_1: 5;

    end;

    

     Lm19: for a,x,y be Element of multEX_0 st a <> ( 0. multEX_0 ) holds (x * a) = (y * a) implies x = y

    proof

      let a,x,y be Element of multEX_0 such that

       A1: a <> ( 0. multEX_0 );

      reconsider aa = a, p = x, q = y as Real;

      assume (x * a) = (y * a);

      

      then (p * aa) = (y * a) by BINOP_2:def 11

      .= (q * aa) by BINOP_2:def 11;

      hence thesis by A1, XCMPLX_1: 5;

    end;

    

     Lm20: for a be Element of multEX_0 holds (a * ( 0. multEX_0 )) = ( 0. multEX_0 )

    proof

      let a be Element of multEX_0 ;

      reconsider aa = a as Real;

      

      thus (a * ( 0. multEX_0 )) = (aa * 0 ) by BINOP_2:def 11

      .= ( 0. multEX_0 );

    end;

    

     Lm21: for a be Element of multEX_0 holds (( 0. multEX_0 ) * a) = ( 0. multEX_0 )

    proof

      let a be Element of multEX_0 ;

      reconsider aa = a as Real;

      

      thus (( 0. multEX_0 ) * a) = ( 0 * aa) by BINOP_2:def 11

      .= ( 0. multEX_0 );

    end;

    definition

      let IT be non empty multLoopStr_0;

      :: ALGSTR_1:def8

      attr IT is almost_invertible means

      : Def8: (for a,b be Element of IT st a <> ( 0. IT) holds ex x be Element of IT st (a * x) = b) & for a,b be Element of IT st a <> ( 0. IT) holds ex x be Element of IT st (x * a) = b;

    end

    definition

      let IT be non empty multLoopStr_0;

      :: ALGSTR_1:def9

      attr IT is multLoop_0-like means IT is almost_invertible almost_cancelable & (for a be Element of IT holds (a * ( 0. IT)) = ( 0. IT)) & for a be Element of IT holds (( 0. IT) * a) = ( 0. IT);

    end

    ::$Canceled

    theorem :: ALGSTR_1:16

    

     Th14: for L be non empty multLoopStr_0 holds L is multLoop_0-like iff (for a,b be Element of L st a <> ( 0. L) holds ex x be Element of L st (a * x) = b) & (for a,b be Element of L st a <> ( 0. L) holds ex x be Element of L st (x * a) = b) & (for a,x,y be Element of L st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a,x,y be Element of L st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a be Element of L holds (a * ( 0. L)) = ( 0. L)) & for a be Element of L holds (( 0. L) * a) = ( 0. L)

    proof

      let L be non empty multLoopStr_0;

      hereby

        assume

         A1: L is multLoop_0-like;

        then

         A2: L is almost_invertible almost_cancelable;

        hence (for a,b be Element of L st a <> ( 0. L) holds ex x be Element of L st (a * x) = b) & for a,b be Element of L st a <> ( 0. L) holds ex x be Element of L st (x * a) = b;

        thus for a,x,y be Element of L st a <> ( 0. L) holds (a * x) = (a * y) implies x = y by A2, ALGSTR_0:def 20, ALGSTR_0:def 36;

        thus for a,x,y be Element of L st a <> ( 0. L) holds (x * a) = (y * a) implies x = y by A2, ALGSTR_0:def 21, ALGSTR_0:def 37;

        thus (for a be Element of L holds (a * ( 0. L)) = ( 0. L)) & for a be Element of L holds (( 0. L) * a) = ( 0. L) by A1;

      end;

      assume that

       A3: (for a,b be Element of L st a <> ( 0. L) holds ex x be Element of L st (a * x) = b) & for a,b be Element of L st a <> ( 0. L) holds ex x be Element of L st (x * a) = b and

       A4: for a,x,y be Element of L st a <> ( 0. L) holds (a * x) = (a * y) implies x = y and

       A5: for a,x,y be Element of L st a <> ( 0. L) holds (x * a) = (y * a) implies x = y and

       A6: (for a be Element of L holds (a * ( 0. L)) = ( 0. L)) & for a be Element of L holds (( 0. L) * a) = ( 0. L);

      

       A7: L is almost_right_cancelable

      proof

        let x be Element of L;

        assume

         A8: x <> ( 0. L);

        let y,z be Element of L;

        assume (y * x) = (z * x);

        hence thesis by A5, A8;

      end;

      L is almost_left_cancelable

      proof

        let x be Element of L;

        assume

         A9: x <> ( 0. L);

        let y,z be Element of L;

        assume (x * y) = (x * z);

        hence thesis by A4, A9;

      end;

      then L is almost_invertible almost_cancelable by A3, A7;

      hence thesis by A6;

    end;

    registration

      cluster multLoop_0-like -> almost_invertible almost_cancelable for non empty multLoopStr_0;

      coherence ;

    end

    registration

      cluster strict well-unital multLoop_0-like non degenerated for non empty multLoopStr_0;

      existence

      proof

         multEX_0 is well-unital multLoop_0-like non degenerated by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Th14;

        hence thesis;

      end;

    end

    definition

      mode multLoop_0 is well-unital non degenerated multLoop_0-like non empty multLoopStr_0;

    end

    registration

      cluster multEX_0 -> well-unital multLoop_0-like;

      coherence by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Th14;

    end

    

     Lm22: for a,b,c be Element of multEX_0 holds ((a * b) * c) = (a * (b * c))

    proof

      let a,b,c be Element of multEX_0 ;

      reconsider p = a, q = b, r = c as Real;

      

       A1: (b * c) = (q * r) by BINOP_2:def 11;

      (a * b) = (p * q) by BINOP_2:def 11;

      

      hence ((a * b) * c) = ((p * q) * r) by BINOP_2:def 11

      .= (p * (q * r))

      .= (a * (b * c)) by A1, BINOP_2:def 11;

    end;

    registration

      cluster strict associative non degenerated for multLoop_0;

      existence

      proof

         multEX_0 is associative non degenerated by Lm22;

        hence thesis;

      end;

    end

    definition

      mode multGroup_0 is associative non degenerated multLoop_0;

    end

    registration

      cluster multEX_0 -> associative;

      coherence by Lm22;

    end

    

     Lm23: for a,b be Element of multEX_0 holds (a * b) = (b * a)

    proof

      let a,b be Element of multEX_0 ;

      reconsider p = a, q = b as Real;

      

      thus (a * b) = (q * p) by BINOP_2:def 11

      .= (b * a) by BINOP_2:def 11;

    end;

    registration

      cluster strict commutative for multGroup_0;

      existence

      proof

         multEX_0 is commutative non degenerated by Lm23;

        hence thesis;

      end;

    end

    notation

      let L be almost_invertible almost_cancelable non empty multLoopStr_0;

      let x be Element of L;

      synonym x " for / x;

    end

    definition

      let L be almost_invertible almost_cancelable non empty multLoopStr_0;

      let x be Element of L;

      assume

       A1: x <> ( 0. L);

      :: original: "

      redefine

      :: ALGSTR_1:def10

      func x " means

      : Def10: (it * x) = ( 1. L);

      compatibility

      proof

        let IT be Element of L;

        ex x1 be Element of L st (x1 * x) = ( 1. L) by A1, Def8;

        then

         A2: x is left_invertible;

        x is right_mult-cancelable by A1, ALGSTR_0:def 37;

        hence thesis by A2, ALGSTR_0:def 30;

      end;

    end

    reserve G for associative almost_invertible almost_cancelable well-unital non empty multLoopStr_0;

    reserve a,x for Element of G;

    theorem :: ALGSTR_1:17

    a <> ( 0. G) implies ((a " ) * a) = ( 1. G) & (a * (a " )) = ( 1. G)

    proof

      assume

       A1: a <> ( 0. G);

      hence

       A2: ((a " ) * a) = ( 1. G) by Def10;

      consider x such that

       A3: (a * x) = ( 1. G) by A1, Def8;

      (((a " ) * a) * x) = ((a " ) * ( 1. G)) by A3, GROUP_1:def 3;

      then x = ((a " ) * ( 1. G)) by A2;

      hence thesis by A3;

    end;

    definition

      let L be almost_invertible almost_cancelable non empty multLoopStr_0;

      let a,b be Element of L;

      :: ALGSTR_1:def11

      func a / b -> Element of L equals (a * (b " ));

      correctness ;

    end

    registration

      cluster -> Abelian add-associative right_zeroed right_complementable for 1 -element addLoopStr;

      coherence

      proof

        let S be 1 -element addLoopStr;

        thus (for v,w be Element of S holds (v + w) = (w + v)) & (for u,v,w be Element of S holds ((u + v) + w) = (u + (v + w))) & for v be Element of S holds (v + ( 0. S)) = v by STRUCT_0:def 10;

        let v be Element of S;

        take v;

        thus thesis by STRUCT_0:def 10;

      end;

      cluster trivial -> well-unital right-distributive for non empty doubleLoopStr;

      coherence ;

    end

    registration

      cluster -> Group-like associative commutative for 1 -element multMagma;

      coherence

      proof

        let H be 1 -element multMagma;

        hereby

          set e = the Element of H;

          take e;

          let h be Element of H;

          thus (h * e) = h & (e * h) = h by STRUCT_0:def 10;

          take g = e;

          thus (h * g) = e & (g * h) = e by STRUCT_0:def 10;

        end;

        thus for x,y,z be Element of H holds ((x * y) * z) = (x * (y * z)) by STRUCT_0:def 10;

        let x,y be Element of H;

        thus thesis by STRUCT_0:def 10;

      end;

    end