realset2.miz



    begin

    definition

      :: REALSET2:def1

      func add_2 -> BinOp of 2 equals ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)) +* ((1, 0 ) .--> 1)) +* ((1,1) .--> 0 ));

      coherence

      proof

        set f2 = ((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)), f1 = (f2 +* ((1, 0 ) .--> 1)), f = (f1 +* ((1,1) .--> 0 ));

        

         A1: ( dom f) = (( dom f1) \/ ( dom ((1,1) .--> 0 ))) by FUNCT_4:def 1

        .= (( dom f1) \/ { [1, 1]}) by FUNCOP_1: 13

        .= ((( dom f2) \/ ( dom ((1, 0 ) .--> 1))) \/ { [1, 1]}) by FUNCT_4:def 1

        .= ((( dom f2) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCOP_1: 13

        .= (((( dom (( 0 , 0 ) .--> 0 )) \/ ( dom (( 0 ,1) .--> 1))) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCT_4:def 1

        .= (((( dom (( 0 , 0 ) .--> 0 )) \/ { [ 0 , 1]}) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCOP_1: 13

        .= ((( { [ 0 , 0 ]} \/ { [ 0 , 1]}) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCOP_1: 13

        .= (( { [ 0 , 0 ], [ 0 , 1]} \/ { [1, 0 ]}) \/ { [1, 1]}) by ENUMSET1: 1

        .= ( { [ 0 , 0 ], [ 0 , 1], [1, 0 ]} \/ { [1, 1]}) by ENUMSET1: 3

        .= { [ 0 , 0 ], [ 0 , 1], [1, 0 ], [1, 1]} by ENUMSET1: 6

        .= [:2, 2:] by CARD_1: 50, ZFMISC_1: 122;

        

         A2: 1 c= 2 by CARD_1: 49, CARD_1: 50, ZFMISC_1: 7;

        ( rng (( 0 , 0 ) .--> 0 )) c= 1 by CARD_1: 49, FUNCOP_1: 13;

        then

         A3: ( rng (( 0 , 0 ) .--> 0 )) c= 2 by A2;

        

         A4: {1} c= 2 by CARD_1: 50, ZFMISC_1: 7;

        ( rng (( 0 ,1) .--> 1)) c= {1} by FUNCOP_1: 13;

        then ( rng (( 0 ,1) .--> 1)) c= 2 by A4;

        then

         A5: (( rng (( 0 , 0 ) .--> 0 )) \/ ( rng (( 0 ,1) .--> 1))) c= 2 by A3, XBOOLE_1: 8;

        ( rng ((1, 0 ) .--> 1)) c= {1} by FUNCOP_1: 13;

        then

         A6: ( rng ((1, 0 ) .--> 1)) c= 2 by A4;

        ( rng f2) c= (( rng (( 0 , 0 ) .--> 0 )) \/ ( rng (( 0 ,1) .--> 1))) by FUNCT_4: 17;

        then ( rng f2) c= 2 by A5;

        then

         A7: (( rng f2) \/ ( rng ((1, 0 ) .--> 1))) c= 2 by A6, XBOOLE_1: 8;

        ( rng ((1,1) .--> 0 )) c= 1 by CARD_1: 49, FUNCOP_1: 13;

        then

         A8: ( rng ((1,1) .--> 0 )) c= 2 by A2;

        ( rng f1) c= (( rng f2) \/ ( rng ((1, 0 ) .--> 1))) by FUNCT_4: 17;

        then ( rng f1) c= 2 by A7;

        then

         A9: (( rng f1) \/ ( rng ((1,1) .--> 0 ))) c= 2 by A8, XBOOLE_1: 8;

        ( rng f) c= (( rng f1) \/ ( rng ((1,1) .--> 0 ))) by FUNCT_4: 17;

        then ( rng f) c= 2 by A9;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

      :: REALSET2:def2

      func mult_2 -> BinOp of 2 equals ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )) +* ((1, 0 ) .--> 0 )) +* ((1,1) .--> 1));

      coherence

      proof

        

         A10: ( rng ((1,1) .--> 1)) c= {1} by FUNCOP_1: 13;

         {1} c= 2 by CARD_1: 50, ZFMISC_1: 7;

        then

         A11: ( rng ((1,1) .--> 1)) c= 2 by A10;

        set f2 = ((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )), f1 = (f2 +* ((1, 0 ) .--> 0 )), f = (f1 +* ((1,1) .--> 1));

        

         A12: ( dom f) = (( dom f1) \/ ( dom ((1,1) .--> 1))) by FUNCT_4:def 1

        .= (( dom f1) \/ { [1, 1]}) by FUNCOP_1: 13

        .= ((( dom f2) \/ ( dom ((1, 0 ) .--> 0 ))) \/ { [1, 1]}) by FUNCT_4:def 1

        .= ((( dom f2) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCOP_1: 13

        .= (((( dom (( 0 , 0 ) .--> 0 )) \/ ( dom (( 0 ,1) .--> 0 ))) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCT_4:def 1

        .= (((( dom (( 0 , 0 ) .--> 0 )) \/ { [ 0 , 1]}) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCOP_1: 13

        .= ((( { [ 0 , 0 ]} \/ { [ 0 , 1]}) \/ { [1, 0 ]}) \/ { [1, 1]}) by FUNCOP_1: 13

        .= (( { [ 0 , 0 ], [ 0 , 1]} \/ { [1, 0 ]}) \/ { [1, 1]}) by ENUMSET1: 1

        .= ( { [ 0 , 0 ], [ 0 , 1], [1, 0 ]} \/ { [1, 1]}) by ENUMSET1: 3

        .= { [ 0 , 0 ], [ 0 , 1], [1, 0 ], [1, 1]} by ENUMSET1: 6

        .= [:2, 2:] by CARD_1: 50, ZFMISC_1: 122;

        

         A13: 1 c= 2 by CARD_1: 49, CARD_1: 50, ZFMISC_1: 7;

        ( rng (( 0 , 0 ) .--> 0 )) c= 1 by CARD_1: 49, FUNCOP_1: 13;

        then

         A14: ( rng (( 0 , 0 ) .--> 0 )) c= 2 by A13;

        ( rng (( 0 ,1) .--> 0 )) c= 1 by CARD_1: 49, FUNCOP_1: 13;

        then ( rng (( 0 ,1) .--> 0 )) c= 2 by A13;

        then

         A15: (( rng (( 0 , 0 ) .--> 0 )) \/ ( rng (( 0 ,1) .--> 0 ))) c= 2 by A14, XBOOLE_1: 8;

        ( rng ((1, 0 ) .--> 0 )) c= 1 by CARD_1: 49, FUNCOP_1: 13;

        then

         A16: ( rng ((1, 0 ) .--> 0 )) c= 2 by A13;

        ( rng f2) c= (( rng (( 0 , 0 ) .--> 0 )) \/ ( rng (( 0 ,1) .--> 0 ))) by FUNCT_4: 17;

        then ( rng f2) c= 2 by A15;

        then

         A17: (( rng f2) \/ ( rng ((1, 0 ) .--> 0 ))) c= 2 by A16, XBOOLE_1: 8;

        ( rng f1) c= (( rng f2) \/ ( rng ((1, 0 ) .--> 0 ))) by FUNCT_4: 17;

        then ( rng f1) c= 2 by A17;

        then

         A18: (( rng f1) \/ ( rng ((1,1) .--> 1))) c= 2 by A11, XBOOLE_1: 8;

        ( rng f) c= (( rng f1) \/ ( rng ((1,1) .--> 1))) by FUNCT_4: 17;

        then ( rng f) c= 2 by A18;

        hence thesis by A12, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    reserve x,y for set;

    set x = ( In ( 0 ,2)), y = ( In (1,2));

    

     Lm1: 1 in 2 by CARD_1: 50, TARSKI:def 2;

    

     Lm2: 0 in 2 by CARD_1: 50, TARSKI:def 2;

    then

     Lm3: x = 0 by SUBSET_1:def 8;

    

     Lm4: y = 1 by Lm1, SUBSET_1:def 8;

    set Z = 2;

    reconsider A = Z as non trivial set by Lm1, Lm2, ZFMISC_1:def 10;

    reconsider nd = x as Element of A;

    

     Lm5: ( dom ((1,1) .--> 0 )) = { [1, 1]} by FUNCOP_1: 13;

    

     Lm6: ( dom ((1, 0 ) .--> 1)) = { [1, 0 ]} by FUNCOP_1: 13;

    

     Lm7: ( dom (( 0 ,1) .--> 1)) = { [ 0 , 1]} by FUNCOP_1: 13;

    

     Lm8: ( add_2 . (x,x)) = x

    proof

       [x, x] <> [ 0 , 1] by Lm3, XTUPLE_0: 1;

      then

       A1: not [x, x] in ( dom (( 0 ,1) .--> 1)) by Lm7, TARSKI:def 1;

       [x, x] <> [1, 0 ] by Lm3, XTUPLE_0: 1;

      then

       A2: not [x, x] in ( dom ((1, 0 ) .--> 1)) by Lm6, TARSKI:def 1;

       [x, x] <> [1, 1] by Lm3, XTUPLE_0: 1;

      then not [x, x] in ( dom ((1,1) .--> 0 )) by Lm5, TARSKI:def 1;

      

      hence ( add_2 . (x,x)) = ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)) +* ((1, 0 ) .--> 1)) . (x,x)) by FUNCT_4: 11

      .= (((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)) . (x,x)) by A2, FUNCT_4: 11

      .= ((( 0 , 0 ) .--> 0 ) . (x,x)) by A1, FUNCT_4: 11

      .= x by Lm3, FUNCOP_1: 71;

    end;

    

     Lm9: ( add_2 . (x,y)) = y

    proof

       [x, y] <> [1, 0 ] by Lm3, XTUPLE_0: 1;

      then

       A1: not [x, y] in ( dom ((1, 0 ) .--> 1)) by Lm6, TARSKI:def 1;

      

       A2: [x, y] in ( dom (( 0 ,1) .--> 1)) by Lm3, Lm4, Lm7, TARSKI:def 1;

       [x, y] <> [1, 1] by Lm3, XTUPLE_0: 1;

      then not [x, y] in ( dom ((1,1) .--> 0 )) by Lm5, TARSKI:def 1;

      

      hence ( add_2 . (x,y)) = ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)) +* ((1, 0 ) .--> 1)) . (x,y)) by FUNCT_4: 11

      .= (((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)) . (x,y)) by A1, FUNCT_4: 11

      .= ((( 0 ,1) .--> 1) . (x,y)) by A2, FUNCT_4: 13

      .= y by Lm3, Lm4, FUNCOP_1: 71;

    end;

    

     Lm10: ( add_2 . (y,x)) = y

    proof

      

       A1: [y, x] in ( dom ((1, 0 ) .--> 1)) by Lm3, Lm4, Lm6, TARSKI:def 1;

       [y, x] <> [1, 1] by Lm3, XTUPLE_0: 1;

      then not [y, x] in ( dom ((1,1) .--> 0 )) by Lm5, TARSKI:def 1;

      

      hence ( add_2 . (y,x)) = ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 1)) +* ((1, 0 ) .--> 1)) . (y,x)) by FUNCT_4: 11

      .= (((1, 0 ) .--> 1) . (y,x)) by A1, FUNCT_4: 13

      .= y by Lm3, Lm4, FUNCOP_1: 71;

    end;

    

     Lm11: ( add_2 . (y,y)) = x

    proof

       [y, y] in ( dom ((1,1) .--> 0 )) by Lm4, Lm5, TARSKI:def 1;

      

      hence ( add_2 . (y,y)) = (((1,1) .--> 0 ) . (y,y)) by FUNCT_4: 13

      .= x by Lm3, Lm4, FUNCOP_1: 71;

    end;

    

     Lm12: ( dom ((1,1) .--> 1)) = { [1, 1]} by FUNCOP_1: 13;

    

     Lm13: ( dom ((1, 0 ) .--> 0 )) = { [1, 0 ]} by FUNCOP_1: 13;

    

     Lm14: ( dom (( 0 ,1) .--> 0 )) = { [ 0 , 1]} by FUNCOP_1: 13;

    

     Lm15: ( mult_2 . (x,x)) = x

    proof

       [x, x] <> [ 0 , 1] by Lm3, XTUPLE_0: 1;

      then

       A1: not [x, x] in ( dom (( 0 ,1) .--> 0 )) by Lm14, TARSKI:def 1;

       [x, x] <> [1, 0 ] by Lm3, XTUPLE_0: 1;

      then

       A2: not [x, x] in ( dom ((1, 0 ) .--> 0 )) by Lm13, TARSKI:def 1;

       [x, x] <> [1, 1] by Lm3, XTUPLE_0: 1;

      then not [x, x] in ( dom ((1,1) .--> 1)) by Lm12, TARSKI:def 1;

      

      hence ( mult_2 . (x,x)) = ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )) +* ((1, 0 ) .--> 0 )) . (x,x)) by FUNCT_4: 11

      .= (((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )) . (x,x)) by A2, FUNCT_4: 11

      .= ((( 0 , 0 ) .--> 0 ) . (x,x)) by A1, FUNCT_4: 11

      .= x by Lm3, FUNCOP_1: 71;

    end;

    

     Lm16: ( mult_2 . (x,y)) = x

    proof

       [x, y] <> [1, 0 ] by Lm3, XTUPLE_0: 1;

      then

       A1: not [x, y] in ( dom ((1, 0 ) .--> 0 )) by Lm13, TARSKI:def 1;

      

       A2: [x, y] in ( dom (( 0 ,1) .--> 0 )) by Lm3, Lm4, Lm14, TARSKI:def 1;

       [x, y] <> [1, 1] by Lm3, XTUPLE_0: 1;

      then not [x, y] in ( dom ((1,1) .--> 1)) by Lm12, TARSKI:def 1;

      

      hence ( mult_2 . (x,y)) = ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )) +* ((1, 0 ) .--> 0 )) . (x,y)) by FUNCT_4: 11

      .= (((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )) . (x,y)) by A1, FUNCT_4: 11

      .= ((( 0 ,1) .--> 0 ) . (x,y)) by A2, FUNCT_4: 13

      .= x by Lm3, Lm4, FUNCOP_1: 71;

    end;

    

     Lm17: ( mult_2 . (y,x)) = x

    proof

      

       A1: [y, x] in ( dom ((1, 0 ) .--> 0 )) by Lm3, Lm4, Lm13, TARSKI:def 1;

       [y, x] <> [1, 1] by Lm3, XTUPLE_0: 1;

      then not [y, x] in ( dom ((1,1) .--> 1)) by Lm12, TARSKI:def 1;

      

      hence ( mult_2 . (y,x)) = ((((( 0 , 0 ) .--> 0 ) +* (( 0 ,1) .--> 0 )) +* ((1, 0 ) .--> 0 )) . (y,x)) by FUNCT_4: 11

      .= (((1, 0 ) .--> 0 ) . (y,x)) by A1, FUNCT_4: 13

      .= x by Lm3, Lm4, FUNCOP_1: 71;

    end;

    

     Lm18: ( mult_2 . (y,y)) = y

    proof

       [y, y] in ( dom ((1,1) .--> 1)) by Lm4, Lm12, TARSKI:def 1;

      

      hence ( mult_2 . (y,y)) = (((1,1) .--> 1) . (y,y)) by FUNCT_4: 13

      .= y by Lm4, FUNCOP_1: 71;

    end;

    set om = mult_2 ;

    

     Lm19: (A \ {x}) = {y} by Lm3, Lm4, CARD_1: 50, ZFMISC_1: 17;

    then

     Lm20: [:(A \ {x}), (A \ {x}):] = { [y, y]} by ZFMISC_1: 29;

    

     Lm21: for t be set holds t in [:(A \ {x}), (A \ {x}):] implies (om . t) in (A \ {x})

    proof

      let t be set;

      assume t in [:(A \ {x}), (A \ {x}):];

      then t = [y, y] by Lm20, TARSKI:def 1;

      hence thesis by Lm18, Lm19, TARSKI:def 1;

    end;

    reconsider nm = y as Element of (A \ {nd}) by Lm19, TARSKI:def 1;

    reconsider od0 = add_2 as BinOp of A;

    reconsider om0 = om as BinOp of A;

    

     Lm22: for a,b,d be Element of A holds ( add_2 . (( add_2 . (a,b)),d)) = ( add_2 . (a,( add_2 . (b,d))))

    proof

      let a,b,d be Element of A;

      

       A1: a = x or a = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

      

       A2: b = x or b = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

      

       A3: d = x or d = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

      per cases by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

        suppose a = x;

        hence thesis by A2, A3, Lm8, Lm9, Lm10, Lm11;

      end;

        suppose b = x;

        hence thesis by A1, A3, Lm8, Lm9, Lm10;

      end;

        suppose d = x;

        hence thesis by A1, A2, Lm8, Lm9, Lm10, Lm11;

      end;

        suppose a = y & b = y & d = y;

        hence thesis by Lm9, Lm10, Lm11;

      end;

    end;

    reconsider dL = doubleLoopStr (# A, od0, om0, nm, nd #) as non empty doubleLoopStr;

    

     Lm23: for a be Element of dL holds (a + ( 0. dL)) = a

    proof

      let a be Element of dL;

      a = x or a = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

      hence thesis by Lm8, Lm10;

    end;

    

     Lm24: for a,b,c be Element of dL holds ((a + b) + c) = (a + (b + c)) by Lm22;

    

     Lm25: for a,b be Element of dL holds (a + b) = (b + a)

    proof

      let a,b be Element of dL;

      a = x & b = x or a = x & b = y or a = y & b = x or a = y & b = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

      hence thesis by Lm9, Lm10;

    end;

    reconsider om1 = om as (A \ {nd}) -subsetpreserving BinOp of A by Lm21, REALSET1:def 4;

    

     Lm26: for B be non empty set, P be BinOp of B, e be Element of B st B = (A \ {nd}) & e = nm holds addLoopStr (# B, P, e #) is AbGroup

    proof

      let B be non empty set, P be BinOp of B, e be Element of B;

      assume that

       A1: B = (A \ {nd}) and

       A2: e = nm;

      

       A3: addLoopStr (# B, P, e #) is right_complementable

      proof

        let a be Element of addLoopStr (# B, P, e #);

        take a;

        thus thesis by A1, A2, Lm19, TARSKI:def 1;

      end;

      for a,b,c be Element of B holds (P . ((P . (a,b)),c)) = (P . (a,(P . (b,c))))

      proof

        let a,b,c be Element of B;

        

         A4: b = y by A1, Lm19, TARSKI:def 1;

        

         A5: c = y by A1, Lm19, TARSKI:def 1;

        a = y by A1, Lm19, TARSKI:def 1;

        hence thesis by A1, A4, A5, Lm19, TARSKI:def 1;

      end;

      then

       A6: for a,b,c be Element of addLoopStr (# B, P, e #) holds ((a + b) + c) = (a + (b + c));

      

       A7: for a,b be Element of addLoopStr (# B, P, e #) holds (a + b) = (b + a)

      proof

        let a,b be Element of addLoopStr (# B, P, e #);

        a = y by A1, Lm19, TARSKI:def 1;

        hence thesis by A1, Lm19, TARSKI:def 1;

      end;

      for a be Element of addLoopStr (# B, P, e #) holds (a + ( 0. addLoopStr (# B, P, e #))) = a

      proof

        let a be Element of addLoopStr (# B, P, e #);

        a = y by A1, Lm19, TARSKI:def 1;

        hence thesis by A1, Lm19, TARSKI:def 1;

      end;

      hence thesis by A3, A6, A7, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

    end;

    

     Lm27: for a,b,d be Element of dL holds (a * (b + d)) = ((a * b) + (a * d)) & ((b + d) * a) = ((b * a) + (d * a))

    proof

      let a,b,d be Element of dL;

      

       A1: a = x & b = x & d = x or a = x & b = x & d = y or a = x & b = y & d = x or a = x & b = y & d = y or a = y & b = x & d = x or a = y & b = x & d = y or a = y & b = y & d = x or a = y & b = y & d = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

      hence (a * (b + d)) = ((a * b) + (a * d)) by Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18;

      thus thesis by A1, Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18;

    end;

    definition

      :: REALSET2:def3

      func dL-Z_2 -> doubleLoopStr equals doubleLoopStr (# 2, add_2 , mult_2 , ( In (1,2)), ( In ( 0 ,2)) #);

      coherence ;

    end

    registration

      cluster dL-Z_2 -> strict non empty non degenerated;

      coherence

      proof

        thus dL-Z_2 is strict;

        thus the carrier of dL-Z_2 is non empty;

         0 in 2 by CARD_1: 50, TARSKI:def 2;

        then

         A1: ( 0. dL-Z_2 ) = 0 by SUBSET_1:def 8;

        1 in 2 by CARD_1: 50, TARSKI:def 2;

        hence ( 0. dL-Z_2 ) <> ( 1. dL-Z_2 ) by A1, SUBSET_1:def 8;

      end;

    end

    registration

      cluster dL-Z_2 -> add-associative distributive;

      coherence

      proof

        for a,b,c be Element of dL-Z_2 holds ((a + b) + c) = (a + (b + c)) by Lm22;

        hence dL-Z_2 is add-associative;

        thus dL-Z_2 is distributive

        proof

          let a,b,d be Element of dL-Z_2 ;

          

           A1: a = x & b = x & d = x or a = x & b = x & d = y or a = x & b = y & d = x or a = x & b = y & d = y or a = y & b = x & d = x or a = y & b = x & d = y or a = y & b = y & d = x or a = y & b = y & d = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

          hence (a * (b + d)) = ((a * b) + (a * d)) by Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18;

          thus thesis by A1, Lm8, Lm9, Lm10, Lm11, Lm15, Lm16, Lm17, Lm18;

        end;

      end;

    end

    registration

      cluster add-associative for non trivial strict doubleLoopStr;

      existence

      proof

        take dL-Z_2 ;

        thus thesis;

      end;

    end

    registration

      cluster the carrier of dL-Z_2 -> natural-membered;

      coherence by CARD_1: 50, TARSKI:def 2;

    end

    registration

      cluster empty for Element of dL-Z_2 ;

      existence

      proof

        reconsider z = 0 as Element of dL-Z_2 by CARD_1: 50, TARSKI:def 2;

        take z;

        thus thesis;

      end;

      cluster non empty for Element of dL-Z_2 ;

      existence

      proof

        reconsider z = 1 as Element of dL-Z_2 by CARD_1: 50, TARSKI:def 2;

        take z;

        thus thesis;

      end;

    end

    definition

      let L be doubleLoopStr;

      :: REALSET2:def4

      attr L is Field-like means

      : Def4: the multF of L is (the carrier of L \ {( 0. L)}) -subsetpreserving & for B be non empty set, P be BinOp of B, e be Element of B holds B = ( NonZero L) & e = ( 1. L) & P = (the multF of L || ( NonZero L)) implies addLoopStr (# B, P, e #) is AbGroup;

    end

    registration

      let A be non empty set, od be BinOp of A, nd be Element of A, om be BinOp of A, nm be Element of A;

      cluster doubleLoopStr (# A, od, om, nm, nd #) -> non empty;

      coherence ;

    end

    

     Lm28: for B be non empty set, P be BinOp of B, e be Element of B st B = (A \ {nd}) & e = nm & P = (om1 ! (A,nd)) holds addLoopStr (# B, P, e #) is AbGroup by Lm26;

    registration

      cluster strict Field-like Abelian distributive add-associative right_zeroed right_complementable for non degenerated doubleLoopStr;

      existence

      proof

        set L = doubleLoopStr (# A, od0, om0, nm, nd #);

        

         A1: ( 0. L) = nd;

        ( 1. L) = nm;

        then

        reconsider L as non degenerated doubleLoopStr by A1, Lm3, Lm4, STRUCT_0:def 8;

        take L;

        thus L is strict;

        thus the multF of L is (the carrier of L \ {( 0. L)}) -subsetpreserving by Lm28;

        L is right_complementable

        proof

          let a be Element of L;

          take a;

          a = x or a = y by Lm3, Lm4, CARD_1: 50, TARSKI:def 2;

          hence thesis by Lm8, Lm11;

        end;

        hence thesis by Lm23, Lm24, Lm25, Lm26, Lm27;

      end;

    end

    registration

      cluster add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible -> Field-like for non degenerated doubleLoopStr;

      coherence

      proof

        let L be non degenerated doubleLoopStr;

        set B = ( NonZero L);

        assume

         A1: L is add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible;

        

         A2: for y be set st y in [:B, B:] holds (the multF of L . y) in B

        proof

          let z be set;

          assume z in [:B, B:];

          then

          consider x,y be object such that

           A3: x in B and

           A4: y in B and

           A5: z = [x, y] by ZFMISC_1: 84;

          reconsider x, y as Element of L by A3, A4;

           not y in {( 0. L)} by A4, XBOOLE_0:def 5;

          then

           A6: y <> ( 0. L) by TARSKI:def 1;

           not x in {( 0. L)} by A3, XBOOLE_0:def 5;

          then x <> ( 0. L) by TARSKI:def 1;

          then (x * y) <> ( 0. L) by A1, A6, VECTSP_1: 12;

          then not (x * y) in {( 0. L)} by TARSKI:def 1;

          hence thesis by A5, XBOOLE_0:def 5;

        end;

        hence the multF of L is (the carrier of L \ {( 0. L)}) -subsetpreserving by REALSET1:def 4;

        reconsider om = the multF of L as (the carrier of L \ {( 0. L)}) -subsetpreserving BinOp of L by A2, REALSET1:def 4;

        let B be non empty set, P be BinOp of B, e be Element of B such that

         A7: B = ( NonZero L) and

         A8: e = ( 1. L) and

         A9: P = (the multF of L || ( NonZero L));

        set K = addLoopStr (# B, P, e #);

        

         A10: K is Abelian

        proof

          let v,w be Element of K;

          reconsider a = v, b = w as Element of L by A7, XBOOLE_0:def 5;

          

           A11: [w, v] in [:B, B:];

           [v, w] in [:B, B:];

          

          hence (v + w) = (a * b) by A7, A9, FUNCT_1: 49

          .= (b * a) by A1, GROUP_1:def 12

          .= (w + v) by A7, A9, A11, FUNCT_1: 49;

        end;

        

         A12: K is right_complementable

        proof

          let v be Element of K;

          reconsider a = v as Element of L by A7, XBOOLE_0:def 5;

           not a in {( 0. L)} by A7, XBOOLE_0:def 5;

          then a <> ( 0. L) by TARSKI:def 1;

          then

          consider b be Element of L such that

           A13: (b * a) = ( 1. L) by A1;

          

           A14: (a * b) = ( 1. L) by A1, A13, GROUP_1:def 12;

          then b <> ( 0. L) by A1, VECTSP_1: 6;

          then not b in {( 0. L)} by TARSKI:def 1;

          then

          reconsider w = b as Element of K by A7, XBOOLE_0:def 5;

          take w;

           [v, w] in [:B, B:];

          hence thesis by A7, A8, A9, A14, FUNCT_1: 49;

        end;

        

         A15: K is add-associative

        proof

          let u,v,w be Element of K;

          reconsider a = u, b = v, c = w as Element of L by A7, XBOOLE_0:def 5;

          

           A16: [v, w] in [:B, B:];

          then (P . (v,w)) in B by FUNCT_2: 5;

          then

           A17: [u, ((om || B) . (v,w))] in [:B, B:] by A7, A9, ZFMISC_1: 87;

          

           A18: [u, v] in [:B, B:];

          then (P . (u,v)) in B by FUNCT_2: 5;

          then [((om || B) . (u,v)), w] in [:B, B:] by A7, A9, ZFMISC_1: 87;

          

          hence ((u + v) + w) = (om . (((om || B) . (u,v)),w)) by A7, A9, FUNCT_1: 49

          .= ((a * b) * c) by A18, FUNCT_1: 49

          .= (a * (b * c)) by A1, GROUP_1:def 3

          .= (om . (u,((om || B) . (v,w)))) by A16, FUNCT_1: 49

          .= (u + (v + w)) by A7, A9, A17, FUNCT_1: 49;

        end;

        K is right_zeroed

        proof

          let v be Element of K;

          reconsider a = v as Element of L by A7, XBOOLE_0:def 5;

           [v, ( 0. K)] in [:B, B:];

          

          hence (v + ( 0. K)) = (a * ( 1. L)) by A7, A8, A9, FUNCT_1: 49

          .= v by A1;

        end;

        hence thesis by A10, A15, A12;

      end;

    end

    deffunc suppf1( Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr) = the carrier of $1;

    definition

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr;

      :: REALSET2:def5

      func omf (F) -> (the carrier of F \ {( 0. F)}) -subsetpreserving BinOp of F equals the multF of F;

      coherence by Def4;

    end

    theorem :: REALSET2:1

    for F be Field holds the addLoopStr of F is AbGroup

    proof

      let F be Field;

      set L = the addLoopStr of F;

      

       A1: L is add-associative

      proof

        let u,v,w be Element of L;

        reconsider a = u, b = v, c = w as Element of F;

        

        thus ((u + v) + w) = ((a + b) + c)

        .= (a + (b + c)) by RLVECT_1:def 3

        .= (u + (v + w));

      end;

      

       A2: L is right_zeroed

      proof

        let v be Element of L;

        reconsider a = v as Element of F;

        

        thus (v + ( 0. L)) = (a + ( 0. F))

        .= v;

      end;

      

       A3: L is right_complementable

      proof

        let v be Element of L;

        reconsider a = v as Element of F;

        consider b be Element of F such that

         A4: (a + b) = ( 0. F) by ALGSTR_0:def 11;

        reconsider w = b as Element of L;

        take w;

        thus thesis by A4;

      end;

      L is Abelian

      proof

        let v,w be Element of L;

        reconsider a = v, b = w as Element of F;

        

        thus (v + w) = (a + b)

        .= (b + a)

        .= (w + v);

      end;

      hence thesis by A1, A2, A3;

    end;

    theorem :: REALSET2:2

    for F be Field, a be Element of F holds (a + ( 0. F)) = a & (( 0. F) + a) = a;

    theorem :: REALSET2:3

    

     Th3: for F be AbGroup, a be Element of F holds ex b be Element of F st (a + b) = ( 0. F) & (b + a) = ( 0. F)

    proof

      let F be AbGroup, a be Element of F;

      consider b be Element of F such that

       A1: (a + b) = ( 0. F) by ALGSTR_0:def 11;

      take b;

      thus (a + b) = ( 0. F) by A1;

      thus thesis by A1;

    end;

    theorem :: REALSET2:4

    

     Th4: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c be Element of ( NonZero F) holds ((a * b) * c) = (a * (b * c))

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c be Element of ( NonZero F);

      set B = ( suppf1(F) \ {( 0. F)});

      set P = (( omf F) ! ( suppf1(F),( 0. F)));

      

       A1: B = ( NonZero F);

      then

      reconsider e = ( 1. F) as Element of B by STRUCT_0: 2;

      reconsider D = addLoopStr (# B, P, e #) as strict AbGroup by A1, Def4;

      reconsider a, b, c as Element of D;

      reconsider x = a, y = b, z = c as Element of F;

      

       A2: (( omf F) || ( suppf1(F) \ {( 0. F)})) is Function of [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):], ( suppf1(F) \ {( 0. F)}) by REALSET1: 7;

      then

       A3: ( dom (( omf F) || ( suppf1(F) \ {( 0. F)}))) = [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):] by FUNCT_2:def 1;

      

       A4: for x,y be Element of ( suppf1(F) \ {( 0. F)}) holds (( omf F) . (x,y)) = (the addF of D . (x,y))

      proof

        let x,y be Element of ( suppf1(F) \ {( 0. F)});

         [x, y] in [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):];

        hence thesis by A3, FUNCT_1: 47;

      end;

      

       A5: for s,t be Element of ( suppf1(F) \ {( 0. F)}) holds (the addF of D . (s,t)) is Element of ( suppf1(F) \ {( 0. F)}) & (( omf F) . (s,t)) is Element of ( suppf1(F) \ {( 0. F)})

      proof

        let s,t be Element of ( suppf1(F) \ {( 0. F)});

        

         A6: [s, t] in [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):];

        consider W be Function of [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):], ( suppf1(F) \ {( 0. F)}) such that

         A7: W = (( omf F) || ( suppf1(F) \ {( 0. F)})) by A2;

        (W . (s,t)) is Element of ( suppf1(F) \ {( 0. F)});

        hence thesis by A3, A6, A7, FUNCT_1: 47;

      end;

      

       A8: for x,y,z be Element of ( suppf1(F) \ {( 0. F)}) holds (( omf F) . ((the addF of D . (x,y)),z)) = (the addF of D . ((the addF of D . (x,y)),z)) & (the addF of D . (x,(( omf F) . (y,z)))) = (( omf F) . (x,(( omf F) . (y,z))))

      proof

        let x,y,z be Element of ( suppf1(F) \ {( 0. F)});

        

         A9: (( omf F) . (y,z)) is Element of ( suppf1(F) \ {( 0. F)}) by A5;

        (the addF of D . (x,y)) is Element of ( suppf1(F) \ {( 0. F)}) by A5;

        hence thesis by A4, A9;

      end;

      ((x * y) * z) = (( omf F) . ((the addF of D . (a,b)),c)) by A4

      .= ((a + b) + c) by A8

      .= (a + (b + c)) by RLVECT_1:def 3

      .= (the addF of D . (a,(( omf F) . (b,c)))) by A4

      .= (x * (y * z)) by A8;

      hence thesis;

    end;

    theorem :: REALSET2:5

    

     Th5: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b be Element of ( NonZero F) holds (a * b) = (b * a)

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b be Element of ( NonZero F);

      set B = ( suppf1(F) \ {( 0. F)});

      set P = (( omf F) ! ( suppf1(F),( 0. F)));

      

       A1: B = ( NonZero F);

      then

      reconsider e = ( 1. F) as Element of B by STRUCT_0: 2;

      reconsider D = addLoopStr (# B, P, e #) as strict AbGroup by A1, Def4;

      reconsider a, b as Element of D;

      reconsider x = a, y = b as Element of F;

      (( omf F) || ( suppf1(F) \ {( 0. F)})) is Function of [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):], ( suppf1(F) \ {( 0. F)}) by REALSET1: 7;

      then

       A2: ( dom (( omf F) || ( suppf1(F) \ {( 0. F)}))) = [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):] by FUNCT_2:def 1;

      

       A3: for x,y be Element of ( suppf1(F) \ {( 0. F)}) holds (( omf F) . (x,y)) = (the addF of D . (x,y))

      proof

        let x,y be Element of ( suppf1(F) \ {( 0. F)});

         [x, y] in [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):];

        hence thesis by A2, FUNCT_1: 47;

      end;

      

      then (x * y) = (a + b)

      .= (b + a)

      .= (y * x) by A3;

      hence thesis;

    end;

    theorem :: REALSET2:6

    

     Th6: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a be Element of ( NonZero F) holds (a * ( 1. F)) = a & (( 1. F) * a) = a

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a be Element of ( NonZero F);

      set B = ( suppf1(F) \ {( 0. F)});

      set P = (( omf F) ! ( suppf1(F),( 0. F)));

      

       A1: B = ( NonZero F);

      then

      reconsider e = ( 1. F) as Element of B by STRUCT_0: 2;

      reconsider D = addLoopStr (# B, P, e #) as strict AbGroup by A1, Def4;

      reconsider a as Element of D;

      (( omf F) || ( suppf1(F) \ {( 0. F)})) is Function of [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):], ( suppf1(F) \ {( 0. F)}) by REALSET1: 7;

      then

       A2: ( dom (( omf F) || ( suppf1(F) \ {( 0. F)}))) = [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):] by FUNCT_2:def 1;

      

       A3: for x,y be Element of ( suppf1(F) \ {( 0. F)}) holds (( omf F) . (x,y)) = (the addF of D . (x,y))

      proof

        let x,y be Element of ( suppf1(F) \ {( 0. F)});

         [x, y] in [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):];

        hence thesis by A2, FUNCT_1: 47;

      end;

      

      then

       A4: (( omf F) . (( 1. F),a)) = (( 0. D) + a)

      .= a;

      (( omf F) . (a,( 1. F))) = (a + ( 0. D)) by A3

      .= a;

      hence thesis by A4;

    end;

    theorem :: REALSET2:7

    

     Th7: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a be Element of ( NonZero F) holds ex b be Element of ( NonZero F) st (a * b) = ( 1. F) & (b * a) = ( 1. F)

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a be Element of ( NonZero F);

      set B = ( suppf1(F) \ {( 0. F)});

      set P = (( omf F) ! ( suppf1(F),( 0. F)));

      

       A1: B = ( NonZero F);

      then

      reconsider e = ( 1. F) as Element of B by STRUCT_0: 2;

       addLoopStr (# B, P, e #) is AbGroup by A1, Def4;

      then

      consider D be strict AbGroup such that

       A2: D = addLoopStr (# B, P, e #);

      reconsider a as Element of D by A2;

      consider b be Element of D such that

       A3: (a + b) = ( 0. D) and

       A4: (b + a) = ( 0. D) by Th3;

      reconsider b as Element of ( NonZero F) by A2;

      take b;

      (( omf F) || ( suppf1(F) \ {( 0. F)})) is Function of [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):], ( suppf1(F) \ {( 0. F)}) by REALSET1: 7;

      then

       A5: ( dom (( omf F) || ( suppf1(F) \ {( 0. F)}))) = [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):] by FUNCT_2:def 1;

      for x,y be Element of ( suppf1(F) \ {( 0. F)}) holds (( omf F) . (x,y)) = (the addF of D . (x,y))

      proof

        let x,y be Element of ( suppf1(F) \ {( 0. F)});

         [x, y] in [:( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}):];

        hence thesis by A2, A5, FUNCT_1: 47;

      end;

      hence thesis by A2, A3, A4;

    end;

    theorem :: REALSET2:8

    for F be Field, x,y be Element of F holds (x + y) = ( 0. F) implies y = (( comp F) . x)

    proof

      let F be Field, x,y be Element of F;

      assume (x + y) = ( 0. F);

      then y = ( - x) by RLVECT_1: 6;

      hence thesis by VECTSP_1:def 13;

    end;

    theorem :: REALSET2:9

    for F be Field, x be Element of F holds x = (( comp F) . (( comp F) . x))

    proof

      let F be Field, x be Element of F;

      

      thus x = ( - ( - x))

      .= (( comp F) . ( - x)) by VECTSP_1:def 13

      .= (( comp F) . (( comp F) . x)) by VECTSP_1:def 13;

    end;

    theorem :: REALSET2:10

    for F be Field, a,b be Element of the carrier of F holds (the addF of F . (a,b)) is Element of the carrier of F & (( omf F) . (a,b)) is Element of the carrier of F & (( comp F) . a) is Element of the carrier of F;

    theorem :: REALSET2:11

    for F be Field, a,b,c be Element of F holds (a * (b - c)) = ((a * b) - (a * c)) by VECTSP_1: 11;

    theorem :: REALSET2:12

    for F be Field, a,b,c be Element of F holds ((a - b) * c) = ((a * c) - (b * c)) by VECTSP_1: 13;

    theorem :: REALSET2:13

    for F be Field, a be Element of F holds (a * ( 0. F)) = ( 0. F);

    theorem :: REALSET2:14

    for F be Field, a be Element of F holds (( 0. F) * a) = ( 0. F);

    theorem :: REALSET2:15

    for F be Field, a,b be Element of F holds ( - (a * b)) = (a * ( - b)) by VECTSP_1: 8;

    theorem :: REALSET2:16

    for F be Field holds (( 1. F) * ( 0. F)) = ( 0. F);

    theorem :: REALSET2:17

    for F be Field holds (( 0. F) * ( 1. F)) = ( 0. F);

    theorem :: REALSET2:18

    for F be Field, a,b be Element of the carrier of F holds (( omf F) . (a,b)) is Element of the carrier of F;

    theorem :: REALSET2:19

    

     Th19: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c be Element of F holds ((a * b) * c) = (a * (b * c))

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c be Element of suppf1(F);

      a = ( 0. F) or b = ( 0. F) or c = ( 0. F) or a is Element of ( NonZero F) & b is Element of ( NonZero F) & c is Element of ( NonZero F) by ZFMISC_1: 56;

      hence thesis by Th4;

    end;

    theorem :: REALSET2:20

    

     Th20: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b be Element of F holds (a * b) = (b * a)

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b be Element of suppf1(F);

      a = ( 0. F) or b = ( 0. F) or a is Element of ( NonZero F) & b is Element of ( NonZero F) by ZFMISC_1: 56;

      hence thesis by Th5;

    end;

    theorem :: REALSET2:21

    

     Th21: for F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a be Element of F holds (a * ( 1. F)) = a & (( 1. F) * a) = a

    proof

      let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a be Element of suppf1(F);

      per cases by ZFMISC_1: 56;

        suppose

         A1: a = ( 0. F);

        hence (a * ( 1. F)) = a;

        thus thesis by A1;

      end;

        suppose a is Element of ( NonZero F);

        hence thesis by Th6;

      end;

    end;

    definition

      let F be Field;

      :: REALSET2:def6

      func revf (F) -> UnOp of ( NonZero F) means

      : Def6: for x be Element of ( NonZero F) holds (( omf F) . (x,(it . x))) = ( 1. F);

      existence

      proof

        defpred Z[ object, object] means (( omf F) . ($1,$2)) = ( 1. F);

        

         A1: for x be object st x in ( suppf1(F) \ {( 0. F)}) holds ex y be object st y in ( suppf1(F) \ {( 0. F)}) & Z[x, y]

        proof

          let x be object;

          assume x in ( suppf1(F) \ {( 0. F)});

          then

          reconsider x as Element of ( NonZero F);

          consider y be Element of ( suppf1(F) \ {( 0. F)}) such that

           A2: (x * y) = ( 1. F) and (y * x) = ( 1. F) by Th7;

          reconsider y as set;

          take y;

          thus thesis by A2;

        end;

        ex C be Function of ( suppf1(F) \ {( 0. F)}), ( suppf1(F) \ {( 0. F)}) st for x be object st x in ( suppf1(F) \ {( 0. F)}) holds Z[x, (C . x)] from FUNCT_2:sch 1( A1);

        then

        consider C be UnOp of ( NonZero F) such that

         A3: for x be object st x in ( suppf1(F) \ {( 0. F)}) holds (( omf F) . (x,(C . x))) = ( 1. F);

        take C;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let C1,C2 be UnOp of ( NonZero F) such that

         A4: for x be Element of ( NonZero F) holds (( omf F) . (x,(C1 . x))) = ( 1. F) and

         A5: for x be Element of ( NonZero F) holds (( omf F) . (x,(C2 . x))) = ( 1. F);

        for x be object st x in ( suppf1(F) \ {( 0. F)}) holds (C1 . x) = (C2 . x)

        proof

          let x be object;

          assume

           A6: x in ( suppf1(F) \ {( 0. F)});

          then

           A7: (C1 . x) is Element of ( NonZero F) by FUNCT_2: 5;

          then

          reconsider a = x, C1a = (C1 . x) as Element of F by A6;

          

           A8: (C2 . x) is Element of ( NonZero F) by A6, FUNCT_2: 5;

          then

          reconsider C2a = (C2 . x) as Element of F;

          (C1 . x) = (C1a * ( 1. F))

          .= (C1a * (a * C2a)) by A5, A6

          .= ((a * C1a) * C2a) by A6, A7, A8, Th4

          .= (( 1. F) * C2a) by A4, A6

          .= (C2 . x);

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: REALSET2:22

    for F be Field, x,y be Element of ( NonZero F) holds (x * y) = ( 1. F) implies y = (( revf F) . x)

    proof

      let F be Field, x,y be Element of ( NonZero F);

      assume

       A1: (x * y) = ( 1. F);

      reconsider rx = (( revf F) . x) as Element of F by XBOOLE_0:def 5;

      y = (y * ( 1. F))

      .= (( omf F) . (y,( 1. F)))

      .= (y * (x * rx)) by Def6

      .= (( 1. F) * rx) by A1, Th4

      .= (( revf F) . x);

      hence thesis;

    end;

    theorem :: REALSET2:23

    for F be Field, x be Element of ( NonZero F) holds x = (( revf F) . (( revf F) . x))

    proof

      let F be Field, x be Element of ( NonZero F);

      reconsider rx = (( revf F) . x) as Element of F by XBOOLE_0:def 5;

      reconsider rrx = (( revf F) . (( revf F) . x)) as Element of F by XBOOLE_0:def 5;

      x = (x * ( 1. F))

      .= (( omf F) . (x,( 1. F)))

      .= (x * (rx * rrx)) by Def6

      .= ((x * rx) * rrx) by Th4

      .= (( omf F) . (( 1. F),(( revf F) . (( revf F) . x)))) by Def6

      .= (( 1. F) * rrx)

      .= (( revf F) . (( revf F) . x));

      hence thesis;

    end;

    theorem :: REALSET2:24

    for F be Field, a,b be Element of ( NonZero F) holds (( omf F) . (a,b)) is Element of ( NonZero F) & (( revf F) . a) is Element of ( NonZero F)

    proof

      let F be Field, a,b be Element of ( NonZero F);

       [a, b] in [:( NonZero F), ( NonZero F):];

      hence thesis by REALSET1:def 4;

    end;

    theorem :: REALSET2:25

    for F be Field, a,b,c be Element of F holds (a + b) = (a + c) implies b = c by RLVECT_1: 8;

    theorem :: REALSET2:26

    for F be Field, a be Element of ( NonZero F), b,c be Element of F holds (a * b) = (a * c) implies b = c

    proof

      let F be Field, a be Element of ( NonZero F), b,c be Element of suppf1(F);

      reconsider x = a as Element of F;

      assume

       A1: (a * b) = (a * c);

      reconsider ra = (( revf F) . a) as Element of F by XBOOLE_0:def 5;

      b = (( 1. F) * b)

      .= (( omf F) . (( 1. F),b))

      .= ((x * ra) * b) by Def6

      .= (ra * (x * c)) by A1, Th19

      .= ((x * ra) * c) by Th19

      .= (( omf F) . (( 1. F),c)) by Def6

      .= (( 1. F) * c)

      .= c;

      hence thesis;

    end;

    registration

      cluster Field-like Abelian distributive add-associative right_zeroed right_complementable -> commutative associative well-unital almost_left_invertible for non degenerated doubleLoopStr;

      coherence

      proof

        let L be non degenerated doubleLoopStr;

        assume

         A1: L is Field-like Abelian distributive add-associative right_zeroed right_complementable;

        then for x,y be Element of L holds (x * y) = (y * x) by Th20;

        hence L is commutative by GROUP_1:def 12;

        for x,y,z be Element of L holds ((x * y) * z) = (x * (y * z)) by A1, Th19;

        hence L is associative by GROUP_1:def 3;

        for x be Element of L holds (x * ( 1. L)) = x & (( 1. L) * x) = x by A1, Th21;

        hence L is well-unital;

        let x be Element of L;

        assume x <> ( 0. L);

        then not x in {( 0. L)} by TARSKI:def 1;

        then

        reconsider x as Element of ( NonZero L) by XBOOLE_0:def 5;

        consider y be Element of ( NonZero L) such that (x * y) = ( 1. L) and

         A2: (y * x) = ( 1. L) by A1, Th7;

        take y;

        thus thesis by A2;

      end;

    end