realset3.miz



    begin

    theorem :: REALSET3:1

    

     Th1: for F be Field holds (( revf F) . ( 1. F)) = ( 1. F)

    proof

      let F be Field;

      

       A1: ( 1. F) is Element of ( NonZero F) by STRUCT_0: 2;

      then (( 1. F) * ( 1. F)) = ( 1. F) by REALSET2: 6;

      hence thesis by A1, REALSET2: 22;

    end;

    theorem :: REALSET3:2

    

     Th2: for F be Field holds for a,b be Element of ( NonZero F) holds (( revf F) . (( omf F) . (a,(( revf F) . b)))) = (( omf F) . (b,(( revf F) . a)))

    proof

      let F be Field;

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

      reconsider revfa = (( revf F) . a), revfb = (( revf F) . b) as Element of ( NonZero F);

      

       A1: (( omf F) . (a,(( revf F) . b))) is Element of ( NonZero F) by REALSET2: 24;

      

       A2: (( omf F) . (b,(( revf F) . a))) is Element of ( NonZero F) by REALSET2: 24;

      (revfb * (b * revfa)) = (revfa * (b * revfb)) by REALSET2: 4

      .= (revfa * (( omf F) . (b,revfb)))

      .= (revfa * ( 1. F)) by REALSET2:def 6

      .= (( revf F) . a) by REALSET2: 6;

      

      then ((a * revfb) * (b * revfa)) = (a * revfa) by A2, REALSET2: 4

      .= (( omf F) . (a,revfa))

      .= ( 1. F) by REALSET2:def 6;

      hence thesis by A1, A2, REALSET2: 22;

    end;

    theorem :: REALSET3:3

    

     Th3: for F be Field, a,b be Element of ( NonZero F) holds (( revf F) . (( omf F) . (a,b))) = (( omf F) . ((( revf F) . a),(( revf F) . b)))

    proof

      let F be Field;

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

      reconsider revfa = (( revf F) . a), revfb = (( revf F) . b) as Element of ( NonZero F);

      

      thus (( revf F) . (( omf F) . (a,b))) = (( revf F) . (( omf F) . (a,(( revf F) . (( revf F) . b))))) by REALSET2: 23

      .= (revfb * revfa) by Th2

      .= (revfa * revfb)

      .= (( omf F) . ((( revf F) . a),(( revf F) . b)));

    end;

    theorem :: REALSET3:4

    

     Th4: for F be Field holds for a,b,c,d be Element of F holds (a - b) = (c - d) iff (a + d) = (b + c)

    proof

      let F be Field;

      let a,b,c,d be Element of F;

      hereby

        assume (a - b) = (c - d);

        

        then ((c - d) + b) = ((a + ( - b)) + b)

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

        .= (a + ( 0. F)) by RLVECT_1: 5

        .= a by RLVECT_1: 4;

        

        hence (a + d) = (((c + b) + ( - d)) + d) by RLVECT_1:def 3

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

        .= ((c + b) + ( 0. F)) by RLVECT_1: 5

        .= (b + c) by RLVECT_1: 4;

      end;

      assume (a + d) = (b + c);

      

      then ((b + c) - d) = (a + (d - d)) by RLVECT_1:def 3

      .= (a + ( 0. F)) by RLVECT_1: 5

      .= a by RLVECT_1: 4;

      

      hence (a - b) = (((c - d) + b) - b) by RLVECT_1:def 3

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

      .= ((c - d) + ( 0. F)) by RLVECT_1: 5

      .= (c - d) by RLVECT_1: 4;

    end;

    theorem :: REALSET3:5

    

     Th5: for F be Field holds for a,c be Element of F holds for b,d be Element of ( NonZero F) holds (( omf F) . (a,(( revf F) . b))) = (( omf F) . (c,(( revf F) . d))) iff (( omf F) . (a,d)) = (( omf F) . (b,c))

    proof

      let F be Field;

      let a,c be Element of F;

      let b,d be Element of ( NonZero F);

      

       A1: (( omf F) . (a,(( revf F) . b))) = (( omf F) . (c,(( revf F) . d))) implies (( omf F) . (a,d)) = (( omf F) . (b,c))

      proof

        reconsider revfb = (( revf F) . b), revfd = (( revf F) . d) as Element of ( NonZero F);

        reconsider crevfd = (c * revfd) as Element of F;

        assume

         A2: (( omf F) . (a,(( revf F) . b))) = (( omf F) . (c,(( revf F) . d)));

        

         A3: c = (c * ( 1. F)) by REALSET2: 21

        .= (( omf F) . (c,(d * revfd))) by REALSET2:def 6

        .= (c * (revfd * d))

        .= ((c * revfd) * d) by REALSET2: 19;

        a = (a * ( 1. F)) by REALSET2: 21

        .= (( omf F) . (a,(b * revfb))) by REALSET2:def 6

        .= (a * (revfb * b))

        .= ((a * revfb) * b) by REALSET2: 19

        .= (b * crevfd) by A2

        .= (( omf F) . (b,(( omf F) . (c,(( revf F) . d)))));

        

        hence (( omf F) . (a,d)) = ((b * (c * revfd)) * d)

        .= (b * ((c * revfd) * d)) by REALSET2: 19

        .= (( omf F) . (b,c)) by A3;

      end;

      (( omf F) . (a,d)) = (( omf F) . (b,c)) implies (( omf F) . (a,(( revf F) . b))) = (( omf F) . (c,(( revf F) . d)))

      proof

        reconsider revfd = (( revf F) . d), revfb = (( revf F) . b) as Element of ( NonZero F);

        reconsider crevfd = (( omf F) . (c,revfd)) as Element of F;

        assume

         A4: (( omf F) . (a,d)) = (( omf F) . (b,c));

        a = (a * ( 1. F)) by REALSET2: 21

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

        .= (a * (d * revfd)) by REALSET2:def 6

        .= ((a * d) * revfd) by REALSET2: 19

        .= ((b * c) * revfd) by A4

        .= (b * (c * revfd)) by REALSET2: 19

        .= (crevfd * b);

        

        hence (( omf F) . (a,(( revf F) . b))) = ((crevfd * b) * revfb)

        .= (crevfd * (b * revfb)) by REALSET2: 19

        .= ((( omf F) . (c,revfd)) * ( 1. F)) by REALSET2:def 6

        .= (( omf F) . (c,(( revf F) . d))) by REALSET2: 21;

      end;

      hence thesis by A1;

    end;

    theorem :: REALSET3:6

    for F be Field holds for a,b be Element of F holds for c,d be Element of ( NonZero F) holds (( omf F) . ((( omf F) . (a,(( revf F) . c))),(( omf F) . (b,(( revf F) . d))))) = (( omf F) . ((( omf F) . (a,b)),(( revf F) . (( omf F) . (c,d)))))

    proof

      let F be Field;

      let a,b be Element of F;

      let c,d be Element of ( NonZero F);

      reconsider revfc = (( revf F) . c), revfd = (( revf F) . d) as Element of ( NonZero F);

      (( omf F) . (c,d)) is Element of ( NonZero F) by REALSET2: 24;

      then

      reconsider revfcd = (( revf F) . (c * d)) as Element of F by REALSET2: 24;

      

      thus (( omf F) . ((( omf F) . (a,(( revf F) . c))),(( omf F) . (b,(( revf F) . d))))) = ((a * revfc) * (b * revfd))

      .= (a * (revfc * (b * revfd))) by REALSET2: 19

      .= (a * (b * (revfc * revfd))) by REALSET2: 19

      .= (( omf F) . (a,(( omf F) . (b,(( revf F) . (( omf F) . (c,d))))))) by Th3

      .= (a * (b * revfcd))

      .= ((a * b) * revfcd) by REALSET2: 19

      .= (( omf F) . ((( omf F) . (a,b)),(( revf F) . (( omf F) . (c,d)))));

    end;

    theorem :: REALSET3:7

    for F be Field holds for a,b be Element of F holds for c,d be Element of ( NonZero F) holds (the addF of F . ((( omf F) . (a,(( revf F) . c))),(( omf F) . (b,(( revf F) . d))))) = (( omf F) . ((the addF of F . ((( omf F) . (a,d)),(( omf F) . (b,c)))),(( revf F) . (( omf F) . (c,d)))))

    proof

      let F be Field;

      let a,b be Element of F;

      let c,d be Element of ( NonZero F);

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

      

       A1: a = (a * ( 1. F)) by REALSET2: 21

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

      .= (a * (d * revfd)) by REALSET2:def 6

      .= ((a * d) * revfd) by REALSET2: 19;

      reconsider revfc = (( revf F) . c), revfd = (( revf F) . d) as Element of ( NonZero F);

      (( omf F) . (c,d)) is Element of ( NonZero F) by REALSET2: 24;

      then

      reconsider revfcd = (( revf F) . (c * d)) as Element of F by REALSET2: 24;

      b = (b * ( 1. F)) by REALSET2: 21

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

      .= (b * (c * revfc)) by REALSET2:def 6

      .= ((b * c) * revfc) by REALSET2: 19;

      

      then

       A2: (( omf F) . (b,(( revf F) . d))) = (((b * c) * revfc) * revfd)

      .= ((b * c) * (revfc * revfd)) by REALSET2: 19

      .= (( omf F) . ((( omf F) . (b,c)),(( revf F) . (( omf F) . (c,d))))) by Th3;

      (( omf F) . (a,(( revf F) . c))) = (((a * d) * revfd) * revfc) by A1

      .= ((a * d) * (revfd * revfc)) by REALSET2: 19

      .= (( omf F) . ((( omf F) . (a,d)),(revfc * revfd)))

      .= (( omf F) . ((( omf F) . (a,d)),(( revf F) . (( omf F) . (c,d))))) by Th3;

      

      hence (the addF of F . ((( omf F) . (a,(( revf F) . c))),(( omf F) . (b,(( revf F) . d))))) = (((a * d) * revfcd) + ((b * c) * revfcd)) by A2

      .= (((a * d) + (b * c)) * revfcd) by VECTSP_1:def 7

      .= (( omf F) . ((the addF of F . ((( omf F) . (a,d)),(( omf F) . (b,c)))),(( revf F) . (( omf F) . (c,d)))));

    end;

    definition

      let F be Field;

      :: REALSET3:def1

      func osf (F) -> BinOp of the carrier of F means

      : Def1: for x,y be Element of F holds (it . (x,y)) = (the addF of F . (x,(( comp F) . y)));

      existence

      proof

        defpred P[ Element of F, Element of F, set] means $3 = (the addF of F . ($1,(( comp F) . $2)));

        

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

        ex f be BinOp of the carrier of F st for x be Element of F holds for y be Element of F holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

        then

        consider S be BinOp of the carrier of F such that

         A2: for x,y be Element of F holds (S . (x,y)) = (the addF of F . (x,(( comp F) . y)));

        take S;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let S1,S2 be BinOp of the carrier of F such that

         A3: for x,y be Element of F holds (S1 . (x,y)) = (the addF of F . (x,(( comp F) . y))) and

         A4: for x,y be Element of F holds (S2 . (x,y)) = (the addF of F . (x,(( comp F) . y)));

        now

          let p be object;

          assume p in [:the carrier of F, the carrier of F:];

          then

          consider x,y be object such that

           A5: x in the carrier of F & y in the carrier of F and

           A6: p = [x, y] by ZFMISC_1:def 2;

          

          thus (S1 . p) = (S1 . (x,y)) by A6

          .= (the addF of F . (x,(( comp F) . y))) by A3, A5

          .= (S2 . (x,y)) by A4, A5

          .= (S2 . p) by A6;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: REALSET3:8

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

    proof

      let F be Field;

      let x be Element of F;

      

      thus (( osf F) . (x,x)) = (the addF of F . (x,(( comp F) . x))) by Def1

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

      .= ( 0. F) by RLVECT_1: 5;

    end;

    theorem :: REALSET3:9

    

     Th9: for F be Field holds for a,b,c be Element of F holds (( omf F) . (a,(( osf F) . (b,c)))) = (( osf F) . ((( omf F) . (a,b)),(( omf F) . (a,c))))

    proof

      let F be Field;

      let a,b,c be Element of F;

      

      thus (( omf F) . (a,(( osf F) . (b,c)))) = (( omf F) . (a,(the addF of F . (b,(( comp F) . c))))) by Def1

      .= (a * (b - c)) by VECTSP_1:def 13

      .= ((a * b) - (a * c)) by REALSET2: 11

      .= (the addF of F . ((( omf F) . (a,b)),(( comp F) . (a * c)))) by VECTSP_1:def 13

      .= (( osf F) . ((( omf F) . (a,b)),(( omf F) . (a,c)))) by Def1;

    end;

    theorem :: REALSET3:10

    for F be Field holds for a,b,c be Element of F holds (( omf F) . ((( osf F) . (a,b)),c)) = (( osf F) . ((( omf F) . (a,c)),(( omf F) . (b,c))))

    proof

      let F be Field;

      let a,b,c be Element of F;

      

      thus (( omf F) . ((( osf F) . (a,b)),c)) = ((( osf F) . (a,b)) * c)

      .= (c * (( osf F) . (a,b)))

      .= (( omf F) . (c,(( osf F) . (a,b))))

      .= (( osf F) . ((c * a),(c * b))) by Th9

      .= (( osf F) . ((a * c),(b * c)))

      .= (( osf F) . ((( omf F) . (a,c)),(( omf F) . (b,c))));

    end;

    theorem :: REALSET3:11

    for F be Field holds for a,b be Element of F holds (( osf F) . (a,b)) = (( comp F) . (( osf F) . (b,a)))

    proof

      let F be Field;

      let a,b be Element of F;

      (( osf F) . (a,b)) = (the addF of F . (a,(( comp F) . b))) by Def1

      .= (a + ( - b)) by VECTSP_1:def 13

      .= ( - (b - a)) by RLVECT_1: 33

      .= (( comp F) . (b + ( - a))) by VECTSP_1:def 13

      .= (( comp F) . (the addF of F . (b,(( comp F) . a)))) by VECTSP_1:def 13;

      hence thesis by Def1;

    end;

    theorem :: REALSET3:12

    for F be Field holds for a,b be Element of F holds (( osf F) . ((( comp F) . a),b)) = (( comp F) . (the addF of F . (a,b)))

    proof

      let F be Field;

      let a,b be Element of F;

      

      thus (( osf F) . ((( comp F) . a),b)) = (the addF of F . ((( comp F) . a),(( comp F) . b))) by Def1

      .= (the addF of F . (( - a),(( comp F) . b))) by VECTSP_1:def 13

      .= (( - a) + ( - b)) by VECTSP_1:def 13

      .= ( - (a + b)) by RLVECT_1: 31

      .= (( comp F) . (the addF of F . (a,b))) by VECTSP_1:def 13;

    end;

    theorem :: REALSET3:13

    

     Th13: for F be Field holds for a,b,c,d be Element of F holds (( osf F) . (a,b)) = (( osf F) . (c,d)) iff (a + d) = (b + c)

    proof

      let F be Field;

      let a,b,c,d be Element of F;

      

       A1: (( osf F) . (c,d)) = (the addF of F . (c,(( comp F) . d))) by Def1

      .= (c - d) by VECTSP_1:def 13;

      (( osf F) . (a,b)) = (the addF of F . (a,(( comp F) . b))) by Def1

      .= (a - b) by VECTSP_1:def 13;

      hence thesis by A1, Th4;

    end;

    theorem :: REALSET3:14

    for F be Field holds for a be Element of F holds (( osf F) . (( 0. F),a)) = (( comp F) . a)

    proof

      let F be Field;

      let a be Element of F;

      

      thus (( osf F) . (( 0. F),a)) = (( 0. F) + (( comp F) . a)) by Def1

      .= (( comp F) . a) by REALSET2: 2;

    end;

    theorem :: REALSET3:15

    

     Th15: for F be Field holds for a be Element of F holds (( osf F) . (a,( 0. F))) = a

    proof

      let F be Field;

      let a be Element of F;

      

      thus (( osf F) . (a,( 0. F))) = (the addF of F . (a,(( comp F) . ( 0. F)))) by Def1

      .= (the addF of F . (a,( - ( 0. F)))) by VECTSP_1:def 13

      .= (a + ( 0. F)) by RLVECT_1: 12

      .= a by REALSET2: 2;

    end;

    theorem :: REALSET3:16

    for F be Field holds for a,b,c be Element of F holds (a + b) = c iff (( osf F) . (c,a)) = b

    proof

      let F be Field;

      let a,b,c be Element of F;

      set d = ( 0. F);

      (c + d) = c & (( osf F) . (b,d)) = b by Th15, REALSET2: 2;

      hence thesis by Th13;

    end;

    theorem :: REALSET3:17

    for F be Field holds for a,b,c be Element of F holds (a + b) = c iff (( osf F) . (c,b)) = a

    proof

      let F be Field;

      let a,b,c be Element of F;

      set d = ( 0. F);

      (c + d) = c & (( osf F) . (a,d)) = a by Th15, REALSET2: 2;

      hence thesis by Th13;

    end;

    theorem :: REALSET3:18

    for F be Field holds for a,b,c be Element of F holds (( osf F) . (a,(( osf F) . (b,c)))) = (the addF of F . ((( osf F) . (a,b)),c))

    proof

      let F be Field;

      let a,b,c be Element of F;

      

      thus (( osf F) . (a,(( osf F) . (b,c)))) = (( osf F) . (a,(the addF of F . (b,(( comp F) . c))))) by Def1

      .= (a + (( comp F) . (b + (( comp F) . c)))) by Def1

      .= (a + (( comp F) . (b + ( - c)))) by VECTSP_1:def 13

      .= (a + ( - (b + ( - c)))) by VECTSP_1:def 13

      .= (a + (( - b) + ( - ( - c)))) by RLVECT_1: 31

      .= (a + ((( comp F) . b) + ( - ( - c)))) by VECTSP_1:def 13

      .= (a + ((( comp F) . b) + (( comp F) . ( - c)))) by VECTSP_1:def 13

      .= (a + ((( comp F) . b) + (( comp F) . (( comp F) . c)))) by VECTSP_1:def 13

      .= (a + ((( comp F) . b) + c)) by REALSET2: 9

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

      .= (the addF of F . ((( osf F) . (a,b)),c)) by Def1;

    end;

    theorem :: REALSET3:19

    for F be Field holds for a,b,c be Element of F holds (( osf F) . (a,(the addF of F . (b,c)))) = (( osf F) . ((( osf F) . (a,b)),c))

    proof

      let F be Field;

      let a,b,c be Element of F;

      

      thus (( osf F) . (a,(the addF of F . (b,c)))) = (the addF of F . (a,(( comp F) . (the addF of F . (b,c))))) by Def1

      .= (a - (b + c)) by VECTSP_1:def 13

      .= ((a - b) - c) by RLVECT_1: 27

      .= (the addF of F . ((the addF of F . (a,( - b))),(( comp F) . c))) by VECTSP_1:def 13

      .= (the addF of F . ((the addF of F . (a,(( comp F) . b))),(( comp F) . c))) by VECTSP_1:def 13

      .= (the addF of F . ((( osf F) . (a,b)),(( comp F) . c))) by Def1

      .= (( osf F) . ((( osf F) . (a,b)),c)) by Def1;

    end;

    definition

      let F be Field;

      :: REALSET3:def2

      func ovf (F) -> Function of [:the carrier of F, ( NonZero F):], the carrier of F means

      : Def2: for x be Element of F, y be Element of ( NonZero F) holds (it . (x,y)) = (( omf F) . (x,(( revf F) . y)));

      existence

      proof

        defpred P[ Element of F, Element of ( NonZero F), set] means $3 = (( omf F) . ($1,(( revf F) . $2)));

        now

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

          (( revf F) . y) is Element of F by XBOOLE_0:def 5;

          then

          reconsider z = (( omf F) . (x,(( revf F) . y))) as Element of F by REALSET2: 10;

          take z;

          thus z = (( omf F) . (x,(( revf F) . y)));

        end;

        then

         A1: for x be Element of F holds for y be Element of ( NonZero F) holds ex z be Element of F st P[x, y, z];

        ex f be Function of [:the carrier of F, ( NonZero F):], the carrier of F st for x be Element of F, y be Element of ( NonZero F) holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be Function of [:the carrier of F, ( NonZero F):], the carrier of F such that

         A2: for x be Element of F, y be Element of ( NonZero F) holds (S1 . (x,y)) = (( omf F) . (x,(( revf F) . y))) and

         A3: for x be Element of F, y be Element of ( NonZero F) holds (S2 . (x,y)) = (( omf F) . (x,(( revf F) . y)));

        now

          let p be object;

          assume p in [:the carrier of F, ( NonZero F):];

          then

          consider x,y be object such that

           A4: x in the carrier of F & y in ( NonZero F) and

           A5: p = [x, y] by ZFMISC_1:def 2;

          (S1 . (x,y)) = (( omf F) . (x,(( revf F) . y))) by A2, A4

          .= (S2 . (x,y)) by A3, A4;

          hence (S1 . p) = (S2 . p) by A5;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: REALSET3:20

    

     Th20: for F be Field holds for x be Element of ( NonZero F) holds (( ovf F) . (x,x)) = ( 1. F)

    proof

      let F be Field;

      let x be Element of ( NonZero F);

      

      thus (( ovf F) . (x,x)) = (( omf F) . (x,(( revf F) . x))) by Def2

      .= ( 1. F) by REALSET2:def 6;

    end;

    theorem :: REALSET3:21

    

     Th21: for F be Field holds for a,b be Element of F holds for c be Element of ( NonZero F) holds (( omf F) . (a,(( ovf F) . (b,c)))) = (( ovf F) . ((( omf F) . (a,b)),c))

    proof

      let F be Field;

      let a,b be Element of F;

      let c be Element of ( NonZero F);

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

      

      thus (( omf F) . (a,(( ovf F) . (b,c)))) = (a * (b * revfc)) by Def2

      .= ((a * b) * revfc) by REALSET2: 19

      .= (( ovf F) . ((( omf F) . (a,b)),c)) by Def2;

    end;

    theorem :: REALSET3:22

    for F be Field holds for a be Element of ( NonZero F) holds (( omf F) . (a,(( ovf F) . (( 1. F),a)))) = ( 1. F) & (( omf F) . ((( ovf F) . (( 1. F),a)),a)) = ( 1. F)

    proof

      let F be Field;

      let a be Element of ( NonZero F);

      

      thus

       A1: (( omf F) . (a,(( ovf F) . (( 1. F),a)))) = (( ovf F) . ((a * ( 1. F)),a)) by Th21

      .= (( ovf F) . (a,a)) by REALSET2: 21

      .= ( 1. F) by Th20;

      

      thus (( omf F) . ((( ovf F) . (( 1. F),a)),a)) = ((( ovf F) . (( 1. F),a)) * a)

      .= (a * (( ovf F) . (( 1. F),a)))

      .= ( 1. F) by A1;

    end;

    theorem :: REALSET3:23

    for F be Field holds for a,b be Element of ( NonZero F) holds (( ovf F) . (a,b)) = (( revf F) . (( ovf F) . (b,a)))

    proof

      let F be Field;

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

      (( ovf F) . (a,b)) = (( omf F) . (a,(( revf F) . b))) by Def2

      .= (( revf F) . (( omf F) . (b,(( revf F) . a)))) by Th2;

      hence thesis by Def2;

    end;

    theorem :: REALSET3:24

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

    proof

      let F be Field;

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

      (( revf F) . a) is Element of F by XBOOLE_0:def 5;

      

      hence (( ovf F) . ((( revf F) . a),b)) = (( omf F) . ((( revf F) . a),(( revf F) . b))) by Def2

      .= (( revf F) . (( omf F) . (a,b))) by Th3;

    end;

    theorem :: REALSET3:25

    

     Th25: for F be Field holds for a,c be Element of F holds for b,d be Element of ( NonZero F) holds (( ovf F) . (a,b)) = (( ovf F) . (c,d)) iff (( omf F) . (a,d)) = (( omf F) . (b,c))

    proof

      let F be Field;

      let a,c be Element of F;

      let b,d be Element of ( NonZero F);

      (( ovf F) . (a,b)) = (( omf F) . (a,(( revf F) . b))) & (( ovf F) . (c,d)) = (( omf F) . (c,(( revf F) . d))) by Def2;

      hence thesis by Th5;

    end;

    theorem :: REALSET3:26

    for F be Field holds for a be Element of ( NonZero F) holds (( ovf F) . (( 1. F),a)) = (( revf F) . a)

    proof

      let F be Field;

      let a be Element of ( NonZero F);

      reconsider revfa = (( revf F) . a) as Element of ( NonZero F);

      

      thus (( ovf F) . (( 1. F),a)) = (( omf F) . (( 1. F),(( revf F) . a))) by Def2

      .= (( 1. F) * revfa)

      .= (( revf F) . a) by REALSET2: 6;

    end;

    theorem :: REALSET3:27

    

     Th27: for F be Field holds for a be Element of F holds (( ovf F) . (a,( 1. F))) = a

    proof

      let F be Field;

      let a be Element of F;

      ( 1. F) is Element of ( NonZero F) by STRUCT_0: 2;

      

      hence (( ovf F) . (a,( 1. F))) = (( omf F) . (a,(( revf F) . ( 1. F)))) by Def2

      .= (a * ( 1. F)) by Th1

      .= a by REALSET2: 21;

    end;

    theorem :: REALSET3:28

    for F be Field holds for a be Element of ( NonZero F) holds for b,c be Element of F holds (( omf F) . (a,b)) = c iff (( ovf F) . (c,a)) = b

    proof

      let F be Field;

      let a be Element of ( NonZero F);

      let b,c be Element of F;

      set d = ( 1. F);

      

       A1: (( omf F) . (c,d)) = (c * ( 1. F))

      .= c by REALSET2: 21;

      ( 1. F) is Element of ( NonZero F) & (( ovf F) . (b,d)) = b by Th27, STRUCT_0: 2;

      hence thesis by A1, Th25;

    end;

    theorem :: REALSET3:29

    for F be Field holds for a,c be Element of F holds for b be Element of ( NonZero F) holds (( omf F) . (a,b)) = c iff (( ovf F) . (c,b)) = a

    proof

      let F be Field;

      let a,c be Element of F;

      let b be Element of ( NonZero F);

      set d = ( 1. F);

      

       A1: (( omf F) . (c,d)) = (c * ( 1. F))

      .= c by REALSET2: 21;

      

       A2: (( omf F) . (b,a)) = (b * a)

      .= (a * b)

      .= (( omf F) . (a,b));

      (( ovf F) . (a,d)) = a & ( 1. F) is Element of ( NonZero F) by Th27, STRUCT_0: 2;

      hence thesis by A1, A2, Th25;

    end;

    theorem :: REALSET3:30

    for F be Field holds for a be Element of F holds for b,c be Element of ( NonZero F) holds (( ovf F) . (a,(( ovf F) . (b,c)))) = (( omf F) . ((( ovf F) . (a,b)),c))

    proof

      let F be Field;

      let a be Element of F;

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

      

       A1: (( omf F) . (b,(( revf F) . c))) is Element of ( NonZero F) by REALSET2: 24;

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

      

      thus (( ovf F) . (a,(( ovf F) . (b,c)))) = (( ovf F) . (a,(( omf F) . (b,(( revf F) . c))))) by Def2

      .= (( omf F) . (a,(( revf F) . (( omf F) . (b,(( revf F) . c)))))) by A1, Def2

      .= (( omf F) . (a,(( omf F) . ((( revf F) . b),(( revf F) . (( revf F) . c)))))) by Th3

      .= (a * (revfb * c)) by REALSET2: 23

      .= ((a * revfb) * c) by REALSET2: 19

      .= (( omf F) . ((( ovf F) . (a,b)),c)) by Def2;

    end;

    theorem :: REALSET3:31

    for F be Field holds for a be Element of F holds for b,c be Element of ( NonZero F) holds (( ovf F) . (a,(( omf F) . (b,c)))) = (( ovf F) . ((( ovf F) . (a,b)),c))

    proof

      let F be Field;

      let a be Element of F;

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

      reconsider revfb = (( revf F) . b), revfc = (( revf F) . c) as Element of F by XBOOLE_0:def 5;

      (( omf F) . (b,c)) is Element of ( NonZero F) by REALSET2: 24;

      

      hence (( ovf F) . (a,(( omf F) . (b,c)))) = (( omf F) . (a,(( revf F) . (( omf F) . (b,c))))) by Def2

      .= (a * (revfb * revfc)) by Th3

      .= ((a * revfb) * revfc) by REALSET2: 19

      .= (( omf F) . ((( ovf F) . (a,b)),(( revf F) . c))) by Def2

      .= (( ovf F) . ((( ovf F) . (a,b)),c)) by Def2;

    end;