field_3.miz

    begin



     Th1: for n be Nat holds n = { m where m be Nat : m < n } by AXIOMS: 4;

    theorem :: FIELD_3:1



     Th2: for n be Nat, x be object st n = {x} holds x = 0

    proof

      let n be Nat, x be object;

      assume

       A1: n = {x};

      then ( card n) = 1 by CARD_1: 30;

      then x in { 0 } by A1, CARD_1: 49, TARSKI:def 1;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FIELD_3:2



     Th3: for n be Nat, x,y be object st n = {x, y} & x <> y holds (x = 0 & y = 1) or (x = 1 & y = 0 )

    proof

      let n be Nat, x,y be object;

      assume

       A1: n = {x, y} & x <> y;

      then ( card n) = 2 by CARD_2: 57;

      then

       A2: x in { 0 , 1} & y in { 0 , 1} by A1, CARD_1: 50, TARSKI:def 2;

      per cases by A2, TARSKI:def 2;

        suppose x = 0 ;

        hence thesis by A1, A2, TARSKI:def 2;

      end;

        suppose x = 1;

        hence thesis by A1, A2, TARSKI:def 2;

      end;

    end;

    theorem :: FIELD_3:3



     Th4: for n be Nat st 1 < n holds ( 0. ( Z/ n)) = 0

    proof

      let n be Nat;

      ( Z/ n) = doubleLoopStr (# ( Segm n), ( addint n), ( multint n), ( In (1,( Segm n))), ( In ( 0 ,( Segm n))) #) by INT_3:def 12;

      hence thesis by NAT_1: 44, SUBSET_1:def 8;

    end;

    theorem :: FIELD_3:4



     Th5: (( 1. ( Z/ 2)) + ( 1. ( Z/ 2))) = ( 0. ( Z/ 2))

    proof



       A1: ( Z/ 2) = doubleLoopStr (# ( Segm 2), ( addint 2), ( multint 2), ( In (1,( Segm 2))), ( In ( 0 ,( Segm 2))) #) by INT_3:def 12;

      ( 1. ( Z/ 2)) = 1 by INT_3: 14;



      hence (( 1. ( Z/ 2)) + ( 1. ( Z/ 2))) = ((1 + 1) mod 2) by A1, GR_CY_1:def 4

      .= 0 by INT_1: 50

      .= ( 0. ( Z/ 2)) by Th4;

    end;

    theorem :: FIELD_3:5



     Th6: for R be Ring, n be non zero Nat holds (( power R) . (( 0. R),n)) = ( 0. R)

    proof

      let R be Ring, n be non zero Nat;

      defpred P[ Nat] means (( power R) . (( 0. R),$1)) = ( 0. R);

      (( power R) . (( 0. R),( 0 + 1))) = ((( power R) . (( 0. R), 0 )) * ( 0. R)) by GROUP_1:def 7

      .= ( 0. R);

      then

       A1: P[1];

       A2:

      now

        let k be non zero Nat;

        assume P[k];

        (( power R) . (( 0. R),(k + 1))) = ((( power R) . (( 0. R),k)) * ( 0. R)) by GROUP_1:def 7

        .= ( 0. R);

        hence P[(k + 1)];

      end;

      for k be non zero Nat holds P[k] from NAT_1:sch 10( A1, A2);

      hence thesis;

    end;

    registration

      cluster ( Z/ 3) -> non degenerated almost_left_invertible;

      coherence by PEPIN: 41;

    end

    registration

      cluster finite for Field;

      existence

      proof

        take ( Z/ 3);

        thus thesis;

      end;

      cluster infinite for Field;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    definition

      let L be non empty doubleLoopStr;

      :: FIELD_3:def1

      attr L is almost_trivial means

      : Def1: for a be Element of L holds a = ( 1. L) or a = ( 0. L);

    end

    registration

      cluster degenerated -> almost_trivial for Ring;

      coherence

      proof

        let R be Ring;

        assume

         A1: R is degenerated;

        now

          let a be Element of R;

          a = (a * ( 1. R))

          .= (a * ( 0. R)) by A1, STRUCT_0:def 8

          .= ( 0. R);

          hence a = ( 1. R) or a = ( 0. R);

        end;

        hence thesis;

      end;

      cluster non almost_trivial for Field;

      existence

      proof

        take F = ( Z/ 3);



         A2: ( Z/ 3) = doubleLoopStr (# ( Segm 3), ( addint 3), ( multint 3), ( In (1,( Segm 3))), ( In ( 0 ,( Segm 3))) #) by INT_3:def 12;

        then

        reconsider t = 2 as Element of ( [#] F) by NAT_1: 44;



         A3: t <> ( 0. F) by A2, NAT_1: 44, SUBSET_1:def 8;

        t <> ( 1. F) by A2, NAT_1: 44, SUBSET_1:def 8;

        hence thesis by A3;

      end;

    end

    theorem :: FIELD_3:6

    for R be Ring holds R is almost_trivial iff (R is degenerated or (R,( Z/ 2)) are_isomorphic )

    proof

      let R be Ring;



       A1: ( Z/ 2) = doubleLoopStr (# ( Segm 2), ( addint 2), ( multint 2), ( In (1,( Segm 2))), ( In ( 0 ,( Segm 2))) #) by INT_3:def 12;

       A2:

      now

        assume R is degenerated or (R,( Z/ 2)) are_isomorphic ;

        per cases ;

          suppose R is degenerated;

          hence R is almost_trivial;

        end;

          suppose (R,( Z/ 2)) are_isomorphic ;

          then

          consider f be Function of R, ( Z/ 2) such that

           A4: f is isomorphism by QUOFIELD:def 23;

          f is monomorphism onto by A4, MOD_4:def 12;

          then

           A5: f is linear one-to-one by MOD_4:def 8;

          now

            let a be Element of R;



             A6: ( dom f) = ( [#] R) by FUNCT_2:def 1;



             A7: ( [#] ( INT.Ring 2)) = 2 by A1, ORDINAL1:def 17;

            per cases by A7, CARD_1: 50, TARSKI:def 2;

              suppose (f . a) = 0 ;



              then (f . a) = ( 0. ( Z/ 2)) by A1

              .= (f . ( 0. R)) by A5, RING_2: 6;

              hence a = ( 1. R) or a = ( 0. R) by A5, A6;

            end;

              suppose (f . a) = 1;



              then (f . a) = ( 1_ ( Z/ 2)) by INT_3: 14

              .= (f . ( 1_ R)) by A5, GROUP_1:def 13

              .= (f . ( 1. R));

              hence a = ( 1. R) or a = ( 0. R) by A5, A6;

            end;

          end;

          hence R is almost_trivial;

        end;

      end;

      set A = the carrier of R, B = the carrier of ( Z/ 2);

      now

        assume that

         A8: R is almost_trivial and

         A9: R is non degenerated;

        set f = { [( 0. R), ( 0. ( Z/ 2))], [( 1. R), ( 1. ( Z/ 2))]};

        now

          let o be object;

          assume o in f;

          per cases by TARSKI:def 2;

            suppose o = [( 0. R), ( 0. ( Z/ 2))];

            hence o in [:A, B:] by ZFMISC_1:def 2;

          end;

            suppose o = [( 1. R), ( 1. ( Z/ 2))];

            hence o in [:A, B:] by ZFMISC_1:def 2;

          end;

        end;

        then

        reconsider f as Subset of [:A, B:] by TARSKI:def 3;

        reconsider f as Relation of A, B;

        now

          let x,y1,y2 be object;

          assume

           A11: [x, y1] in f & [x, y2] in f;

          per cases by TARSKI:def 2;

            suppose

             A12: [x, y1] = [( 0. R), ( 0. ( Z/ 2))];



             A13: y1 = ( [( 0. R), ( 0. ( Z/ 2))] `2 ) by A12

            .= ( 0. ( Z/ 2));



             A14: x = ( [( 0. R), ( 0. ( Z/ 2))] `1 ) by A12

            .= ( 0. R);

            per cases by A11, TARSKI:def 2;

              suppose [x, y2] = [( 0. R), ( 0. ( Z/ 2))];



              then y2 = ( [( 0. R), ( 0. ( Z/ 2))] `2 )

              .= ( 0. ( Z/ 2));

              hence y1 = y2 by A13;

            end;

              suppose [x, y2] = [( 1. R), ( 1. ( Z/ 2))];



              then x = ( [( 1. R), ( 1. ( Z/ 2))] `1 )

              .= ( 1. R);

              hence y1 = y2 by A14, A9;

            end;

          end;

            suppose

             A15: [x, y1] = [( 1. R), ( 1. ( Z/ 2))];



            then

             A16: y1 = ( [( 1. R), ( 1. ( Z/ 2))] `2 )

            .= ( 1. ( Z/ 2));



             A17: x = ( [( 1. R), ( 1. ( Z/ 2))] `1 ) by A15

            .= ( 1. R);

            per cases by A11, TARSKI:def 2;

              suppose [x, y2] = [( 0. R), ( 0. ( Z/ 2))];



              then x = ( [( 0. R), ( 0. ( Z/ 2))] `1 )

              .= ( 0. R);

              hence y1 = y2 by A17, A9;

            end;

              suppose [x, y2] = [( 1. R), ( 1. ( Z/ 2))];



              then y2 = ( [( 1. R), ( 1. ( Z/ 2))] `2 )

              .= ( 1. ( Z/ 2));

              hence y1 = y2 by A16;

            end;

          end;

        end;

        then

        reconsider f as PartFunc of A, B by FUNCT_1:def 1;



         A18: ( dom f) c= A;

        now

          let o be object;

          assume o in A;

          then

          reconsider a = o as Element of R;

          per cases by A8;

            suppose a = ( 0. R);

            then [a, ( 0. ( Z/ 2))] in f by TARSKI:def 2;

            hence o in ( dom f) by FUNCT_1: 1;

          end;

            suppose a = ( 1. R);

            then [a, ( 1. ( Z/ 2))] in f by TARSKI:def 2;

            hence o in ( dom f) by FUNCT_1: 1;

          end;

        end;

        then

         A19: ( dom f) = A by A18, TARSKI: 2;

        reconsider f as Function of A, B by A19, FUNCT_2:def 1;



         A20: (f . ( 0. R)) = ( 0. ( Z/ 2)) & (f . ( 1. R)) = ( 1. ( Z/ 2))

        proof

           [( 0. R), ( 0. ( Z/ 2))] in f by TARSKI:def 2;

          hence (f . ( 0. R)) = ( 0. ( Z/ 2)) by A19, FUNCT_1:def 2;

           [( 1. R), ( 1. ( Z/ 2))] in f by TARSKI:def 2;

          hence (f . ( 1. R)) = ( 1. ( Z/ 2)) by A19, FUNCT_1:def 2;

        end;

         A21:

        now

          let a,b be Element of R;

          per cases by A8;

            suppose a = ( 0. R);

            hence (f . (a + b)) = ((f . a) + (f . b)) by A20;

          end;

            suppose

             A22: a = ( 1. R);

            per cases by A8;

              suppose b = ( 0. R);

              hence (f . (a + b)) = ((f . a) + (f . b)) by A20;

            end;

              suppose

               A23: b = ( 1. R);

              now

                assume

                 A24: (a + b) = ( 1. R);

                consider y be Element of R such that

                 A25: (a + y) = ( 0. R) by ALGSTR_0:def 11;

                per cases by A8;

                  suppose y = ( 0. R);

                  hence contradiction by A20, A22, A25;

                end;

                  suppose y = ( 1. R);

                  hence contradiction by A24, A25, A23, A20;

                end;

              end;

              hence (f . (a + b)) = ((f . a) + (f . b)) by A8, A20, Th5, A23, A22;

            end;

          end;

        end;

        now

          let a,b be Element of R;

          per cases by A8;

            suppose a = ( 0. R);

            hence (f . (a * b)) = ((f . a) * (f . b)) by A20;

          end;

            suppose a = ( 1. R);

            hence (f . (a * b)) = ((f . a) * (f . b)) by A20;

          end;

        end;

        then

         A28: f is additive multiplicative unity-preserving by A20, A21, GROUP_6:def 6;

        now

          let x,y be object;

          assume

           A29: x in A & y in A & (f . x) = (f . y);

          then

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

          per cases by A8;

            suppose a = ( 0. R);

            hence x = y by A8, A20, A29;

          end;

            suppose a = ( 1. R);

            hence x = y by A8, A20, A29;

          end;

        end;

        then f is one-to-one by FUNCT_2: 19;

        then

         A30: f is monomorphism by A28, MOD_4:def 8;

         A31:

        now

          let o be object;

          assume o in ( rng f);

          then

          consider x be object such that

           A32: x in ( dom f) & o = (f . x) by FUNCT_1:def 3;

          reconsider a = x as Element of R by A32;

          per cases by A8;

            suppose a = ( 0. R);

            hence o in B by A20, A32;

          end;

            suppose a = ( 1. R);

            hence o in B by A20, A32;

          end;

        end;

        now

          let o be object;

          assume o in B;

          then

           A33: o in 2 by A1, ORDINAL1:def 17;

          per cases by A33, CARD_1: 50, TARSKI:def 2;

            suppose o = 0 ;

            then o = (f . ( 0. R)) by A1, A20, NAT_1: 44, SUBSET_1:def 8;

            hence o in ( rng f) by A19, FUNCT_1:def 3;

          end;

            suppose o = 1;

            then o = (f . ( 1. R)) by A20, A1, NAT_1: 44, SUBSET_1:def 8;

            hence o in ( rng f) by A19, FUNCT_1:def 3;

          end;

        end;

        then f is onto by A31, TARSKI: 2;

        hence (R,( Z/ 2)) are_isomorphic by A30, MOD_4:def 12, QUOFIELD:def 23;

      end;

      hence thesis by A2;

    end;

    definition

      let R be Ring;

      let a be Element of R;

      :: FIELD_3:def2

      attr a is trivial means

      : Def2: a = ( 1. R) or a = ( 0. R);

    end

    registration

      let R be non almost_trivial Ring;

      cluster non trivial for Element of R;

      existence

      proof

        consider a be Element of R such that

         A1: a <> ( 1. R) & a <> ( 0. R) by Def1;

        take a;

        thus thesis by A1;

      end;

    end

    definition

      let R be Ring;

      :: FIELD_3:def3

      attr R is polynomial_disjoint means

      : Def3: (( [#] R) /\ ( [#] ( Polynom-Ring R))) = {} ;

    end

    begin

    definition

      let R be non almost_trivial Ring;

      let x be non trivial Element of R;

      let o be object;

      :: FIELD_3:def4

      func carr (x,o) -> non empty set equals ((( [#] R) \ {x}) \/ {o});

      coherence ;

    end

    definition

      let R be non almost_trivial Ring;

      let x be non trivial Element of R;

      let o be object;

      let a,b be Element of ( carr (x,o));

      :: FIELD_3:def5

      func addR (a,b) -> Element of ( carr (x,o)) equals

      : Def4: (the addF of R . (x,x)) if a = o & b = o & (the addF of R . (x,x)) <> x,

(the addF of R . (a,x)) if a <> o & b = o & (the addF of R . (a,x)) <> x,

(the addF of R . (x,b)) if a = o & b <> o & (the addF of R . (x,b)) <> x,

(the addF of R . (a,b)) if a <> o & b <> o & (the addF of R . (a,b)) <> x

      otherwise o;

      coherence

      proof

         A1:

        now

          assume a = o & b = o & (the addF of R . (x,x)) <> x;

          then not (the addF of R . (x,x)) in {x} by TARSKI:def 1;

          then (the addF of R . (x,x)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the addF of R . (x,x)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

         A2:

        now

          assume

           A3: a <> o & b = o & (the addF of R . (a,x)) <> x;

          then not a in {o} by TARSKI:def 1;

          then a in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider a1 = a as Element of ( [#] R);

           not (the addF of R . (a,x)) in {x} by A3, TARSKI:def 1;

          then (the addF of R . (a1,x)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the addF of R . (a,x)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

         A4:

        now

          assume

           A5: a = o & b <> o & (the addF of R . (x,b)) <> x;

          then not b in {o} by TARSKI:def 1;

          then b in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider b1 = b as Element of ( [#] R);

           not (the addF of R . (x,b)) in {x} by A5, TARSKI:def 1;

          then (the addF of R . (x,b1)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the addF of R . (x,b)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

         A6:

        now

          assume

           A7: a <> o & b <> o & (the addF of R . (a,b)) <> x;

          then not a in {o} by TARSKI:def 1;

          then a in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider a1 = a as Element of ( [#] R);

           not b in {o} by A7, TARSKI:def 1;

          then b in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider b1 = b as Element of ( [#] R);

           not (the addF of R . (a,b)) in {x} by A7, TARSKI:def 1;

          then (the addF of R . (a1,b1)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the addF of R . (a,b)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

        o in {o} by TARSKI:def 1;

        hence thesis by A1, A2, A4, A6, XBOOLE_0:def 3;

      end;

      consistency ;

    end

    definition

      let R be non almost_trivial Ring;

      let x be non trivial Element of R;

      let o be object;

      :: FIELD_3:def6

      func addR (x,o) -> BinOp of ( carr (x,o)) means

      : Def5: for a,b be Element of ( carr (x,o)) holds (it . (a,b)) = ( addR (a,b));

      existence

      proof

        deffunc O( Element of ( carr (x,o)), Element of ( carr (x,o))) = ( addR ($1,$2));

        consider F be BinOp of ( carr (x,o)) such that

         A1: for a,b be Element of ( carr (x,o)) holds (F . (a,b)) = O(a,b) from BINOP_1:sch 4;

        take F;

        let a,b be Element of ( carr (x,o));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( carr (x,o)) such that

         A2: for a,b be Element of ( carr (x,o)) holds (F1 . (a,b)) = ( addR (a,b)) and

         A3: for a,b be Element of ( carr (x,o)) holds (F2 . (a,b)) = ( addR (a,b));

        now

          let a,b be Element of ( carr (x,o));



          thus (F1 . (a,b)) = ( addR (a,b)) by A2

          .= (F2 . (a,b)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let R be non almost_trivial Ring;

      let x be non trivial Element of R;

      let o be object;

      let a,b be Element of ( carr (x,o));

      :: FIELD_3:def7

      func multR (a,b) -> Element of ( carr (x,o)) equals

      : Def6: (the multF of R . (x,x)) if a = o & b = o & (the multF of R . (x,x)) <> x,

(the multF of R . (a,x)) if a <> o & b = o & (the multF of R . (a,x)) <> x,

(the multF of R . (x,b)) if a = o & b <> o & (the multF of R . (x,b)) <> x,

(the multF of R . (a,b)) if a <> o & b <> o & (the multF of R . (a,b)) <> x

      otherwise o;

      coherence

      proof

         A1:

        now

          assume a = o & b = o & (the multF of R . (x,x)) <> x;

          then not (the multF of R . (x,x)) in {x} by TARSKI:def 1;

          then (the multF of R . (x,x)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the multF of R . (x,x)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

         A2:

        now

          assume

           A3: a <> o & b = o & (the multF of R . (a,x)) <> x;

          then not a in {o} by TARSKI:def 1;

          then a in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider a1 = a as Element of ( [#] R);

           not (the multF of R . (a,x)) in {x} by A3, TARSKI:def 1;

          then (the multF of R . (a1,x)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the multF of R . (a,x)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

         A4:

        now

          assume

           A5: a = o & b <> o & (the multF of R . (x,b)) <> x;

          then not b in {o} by TARSKI:def 1;

          then b in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider b1 = b as Element of ( [#] R);

           not (the multF of R . (x,b)) in {x} by A5, TARSKI:def 1;

          then (the multF of R . (x,b1)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the multF of R . (x,b)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

         A6:

        now

          assume

           A7: a <> o & b <> o & (the multF of R . (a,b)) <> x;

          then not a in {o} by TARSKI:def 1;

          then a in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider a1 = a as Element of ( [#] R);

           not b in {o} by A7, TARSKI:def 1;

          then b in (( [#] R) \ {x}) by XBOOLE_0:def 3;

          then

          reconsider b1 = b as Element of ( [#] R);

           not (the multF of R . (a,b)) in {x} by A7, TARSKI:def 1;

          then (the multF of R . (a1,b1)) in (( [#] R) \ {x}) by XBOOLE_0:def 5;

          hence (the multF of R . (a,b)) is Element of ( carr (x,o)) by XBOOLE_0:def 3;

        end;

        o in {o} by TARSKI:def 1;

        hence thesis by A1, A2, A4, A6, XBOOLE_0:def 3;

      end;

      consistency ;

    end

    definition

      let R be non almost_trivial Ring;

      let x be non trivial Element of R;

      let o be object;

      :: FIELD_3:def8

      func multR (x,o) -> BinOp of ( carr (x,o)) means

      : Def7: for a,b be Element of ( carr (x,o)) holds (it . (a,b)) = ( multR (a,b));

      existence

      proof

        deffunc O( Element of ( carr (x,o)), Element of ( carr (x,o))) = ( multR ($1,$2));

        consider F be BinOp of ( carr (x,o)) such that

         A1: for a,b be Element of ( carr (x,o)) holds (F . (a,b)) = O(a,b) from BINOP_1:sch 4;

        take F;

        let a,b be Element of ( carr (x,o));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( carr (x,o)) such that

         A2: for a,b be Element of ( carr (x,o)) holds (F1 . (a,b)) = ( multR (a,b)) and

         A3: for a,b be Element of ( carr (x,o)) holds (F2 . (a,b)) = ( multR (a,b));

        now

          let a,b be Element of ( carr (x,o));



          thus (F1 . (a,b)) = ( multR (a,b)) by A2

          .= (F2 . (a,b)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let F be non almost_trivial Field;

      let x be non trivial Element of F;

      let o be object;

      :: FIELD_3:def9

      func ExField (x,o) -> strict doubleLoopStr means

      : Def8: the carrier of it = ( carr (x,o)) & the addF of it = ( addR (x,o)) & the multF of it = ( multR (x,o)) & the OneF of it = ( 1. F) & the ZeroF of it = ( 0. F);

      existence

      proof

        ( 1. F) <> x by Def2;

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

        then ( 1. F) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

        then

        reconsider e = ( 1. F) as Element of ( carr (x,o)) by XBOOLE_0:def 3;

        ( 0. F) <> x by Def2;

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

        then ( 0. F) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

        then

        reconsider u = ( 0. F) as Element of ( carr (x,o)) by XBOOLE_0:def 3;

        take doubleLoopStr (# ( carr (x,o)), ( addR (x,o)), ( multR (x,o)), e, u #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F be non almost_trivial Field;

      let x be non trivial Element of F;

      let o be object;

      cluster ( ExField (x,o)) -> non degenerated;

      coherence

      proof

        ( 0. ( ExField (x,o))) = ( 0. F) & ( 1. ( ExField (x,o))) = ( 1. F) by Def8;

        hence thesis by STRUCT_0:def 8;

      end;

    end

    registration

      let F be non almost_trivial Field;

      let x be non trivial Element of F;

      let o be object;

      cluster ( ExField (x,o)) -> Abelian;

      coherence

      proof

        set R = F;



         A1: ( [#] ( ExField (x,o))) = ( carr (x,o)) by Def8;

        now

          let a,b be Element of ( ExField (x,o));

          per cases ;

            suppose

             A2: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of ( carr (x,o)) by XBOOLE_0:def 3;

            per cases ;

              suppose

               A3: a = o;

              then a in {o} by TARSKI:def 1;

              then

              reconsider a1 = a as Element of ( carr (x,o)) by XBOOLE_0:def 3;

              thus (a + b) = (b + a) by A2, A3;

            end;

              suppose

               A4: a <> o;

              then not a in {o} by TARSKI:def 1;

              then

               A5: a in (( [#] R) \ {x}) by A1, XBOOLE_0:def 3;

              reconsider a1 = a as Element of ( carr (x,o)) by Def8;

              reconsider aR = a as Element of R by A5;



               A6: (the addF of R . (a1,x)) = (aR + x)

              .= (x + aR)

              .= (the addF of R . (x,a1));

              per cases ;

                suppose

                 A7: (the addF of R . (a,x)) <> x;



                thus (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

                .= ( addR (a1,b1)) by Def5

                .= (the addF of R . (a,x)) by A7, A4, A2, Def4

                .= ( addR (b1,a1)) by A2, A4, A6, A7, Def4

                .= (( addR (x,o)) . (b1,a1)) by Def5

                .= (b + a) by Def8;

              end;

                suppose

                 A8: (the addF of R . (a,x)) = x;



                thus (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

                .= ( addR (a1,b1)) by Def5

                .= o by A8, A4, A2, Def4

                .= ( addR (b1,a1)) by A6, A8, A4, A2, Def4

                .= (( addR (x,o)) . (b1,a1)) by Def5

                .= (b + a) by Def8;

              end;

            end;

          end;

            suppose

             A9: b <> o;

            then not b in {o} by TARSKI:def 1;

            then

             A10: b in (( [#] R) \ {x}) by A1, XBOOLE_0:def 3;

            reconsider b1 = b as Element of ( carr (x,o)) by Def8;

            per cases ;

              suppose

               A11: a = o;

              then a in {o} by TARSKI:def 1;

              then

              reconsider a1 = a as Element of ( carr (x,o)) by XBOOLE_0:def 3;

              reconsider bR = b as Element of R by A10;



               A12: (the addF of R . (x,b1)) = (x + bR)

              .= (bR + x)

              .= (the addF of R . (b1,x));

              per cases ;

                suppose

                 A13: (the addF of R . (x,b)) <> x;



                thus (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

                .= ( addR (a1,b1)) by Def5

                .= (the addF of R . (x,b)) by A13, A11, A9, Def4

                .= ( addR (b1,a1)) by A9, A11, A12, A13, Def4

                .= (( addR (x,o)) . (b1,a1)) by Def5

                .= (b + a) by Def8;

              end;

                suppose

                 A14: (the addF of R . (x,b)) = x;



                thus (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

                .= ( addR (a1,b1)) by Def5

                .= o by A9, A11, A14, Def4

                .= ( addR (b1,a1)) by A9, A11, A12, A14, Def4

                .= (( addR (x,o)) . (b1,a1)) by Def5

                .= (b + a) by Def8;

              end;

            end;

              suppose

               A15: a <> o;

              then not a in {o} by TARSKI:def 1;

              then

               A16: a in (( [#] R) \ {x}) by A1, XBOOLE_0:def 3;

              reconsider a1 = a as Element of ( carr (x,o)) by Def8;

              reconsider aR = a, bR = b as Element of ( [#] R) by A10, A16;



               A17: (the addF of R . (a,b)) = (aR + bR)

              .= (bR + aR)

              .= (the addF of R . (b,a));

              per cases ;

                suppose

                 A18: (the addF of R . (a,b)) <> x;



                thus (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

                .= ( addR (a1,b1)) by Def5

                .= (the addF of R . (a,b)) by A9, A15, A18, Def4

                .= ( addR (b1,a1)) by A9, A15, A17, A18, Def4

                .= (( addR (x,o)) . (b1,a1)) by Def5

                .= (b + a) by Def8;

              end;

                suppose

                 A19: (the addF of R . (a,b)) = x;



                thus (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

                .= ( addR (a1,b1)) by Def5

                .= o by A9, A15, A19, Def4

                .= ( addR (b1,a1)) by A9, A15, A17, A19, Def4

                .= (( addR (x,o)) . (b1,a1)) by Def5

                .= (b + a) by Def8;

              end;

            end;

          end;

        end;

        hence ( ExField (x,o)) is Abelian by RLVECT_1:def 2;

      end;

    end

    reserve o for object;

    reserve F for non almost_trivial Field;

    reserve x,a for Element of F;

    theorem :: FIELD_3:7



     Th7: for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( ExField (x,o)) is right_zeroed right_complementable

    proof

      let x be non trivial Element of F, o be object;

      assume

       a1: not o in ( [#] F);

      then

       A1: a <> o;

      set C = ( carr (x,o));

      set ADDR = the addF of F;

      consider xi be Element of F such that

       A2: (x + xi) = ( 0. F) by ALGSTR_0:def 11;



       A3: ( [#] ( ExField (x,o))) = C by Def8;

      o in {o} by TARSKI:def 1;

      then

      reconsider u1 = o as Element of C by XBOOLE_0:def 3;

      reconsider u = u1 as Element of ( ExField (x,o)) by Def8;

      now

        let a be Element of ( ExField (x,o));



         A4: ( 0. ( ExField (x,o))) = ( 0. F) by Def8;

        ( 0. F) <> x by Def2;

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

        then ( 0. F) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

        then

        reconsider u = ( 0. F) as Element of C by XBOOLE_0:def 3;



         A5: o <> u by a1;

        per cases ;

          suppose

           A6: a = o;

          then a in {o} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of C by XBOOLE_0:def 3;



           A7: (the addF of F . (x,( 0. F))) = (x + ( 0. F))

          .= x;



          thus (a + ( 0. ( ExField (x,o)))) = (( addR (x,o)) . (a1,u)) by A4, Def8

          .= ( addR (a1,u)) by Def5

          .= a by A5, A6, A7, Def4;

        end;

          suppose

           A8: a <> o;

          then not a in {o} by TARSKI:def 1;

          then

           A9: a in (( [#] F) \ {x}) by A3, XBOOLE_0:def 3;

          reconsider a1 = a as Element of C by Def8;

          reconsider aR = a as Element of ( [#] F) by A9;



           A10: (the addF of F . (a,u)) = (aR + ( 0. F))

          .= aR;

           not aR in {x} by A9, XBOOLE_0:def 5;

          then

           A11: (the addF of F . (a,u)) <> x by A10, TARSKI:def 1;



          thus (a + ( 0. ( ExField (x,o)))) = (( addR (x,o)) . (a1,u)) by A4, Def8

          .= ( addR (a1,u)) by Def5

          .= (aR + ( 0. F)) by A8, A5, A11, Def4

          .= a;

        end;

      end;

      hence ( ExField (x,o)) is right_zeroed by RLVECT_1:def 4;

      now

        let a be Element of ( ExField (x,o));

        per cases ;

          suppose

           A12: a = o;

          then a in {o} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of C by XBOOLE_0:def 3;

          per cases ;

            suppose

             A13: xi = x;

            then

             A14: (the addF of F . (x,x)) <> x by A2, Def2;

            (a + u) = (( addR (x,o)) . (a1,u1)) by Def8

            .= ( addR (a1,u1)) by Def5

            .= (the addF of F . (x,xi)) by A12, A13, A14, Def4

            .= ( 0. ( ExField (x,o))) by A2, Def8;

            hence a is right_complementable by ALGSTR_0:def 11;

          end;

            suppose xi <> x;

            then not xi in {x} by TARSKI:def 1;

            then xi in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider x1i = xi as Element of ( carr (x,o)) by XBOOLE_0:def 3;

            reconsider b = x1i as Element of ( ExField (x,o)) by Def8;



             A15: (the addF of F . (x,b)) <> x by A2, Def2;

            (a + b) = (( addR (x,o)) . (a1,x1i)) by Def8

            .= ( addR (a1,x1i)) by Def5

            .= (the addF of F . (x,xi)) by A1, A12, A15, Def4

            .= ( 0. ( ExField (x,o))) by A2, Def8;

            hence a is right_complementable by ALGSTR_0:def 11;

          end;

        end;

          suppose

           A16: a <> o;

          then not a in {o} by TARSKI:def 1;

          then

           A17: a in (( [#] F) \ {x}) by A3, XBOOLE_0:def 3;

          reconsider a1 = a as Element of C by Def8;

          reconsider aR = a as Element of ( [#] F) by A17;

          consider aRi be Element of F such that

           A18: (aR + aRi) = ( 0. F) by ALGSTR_0:def 11;

          per cases ;

            suppose

             A19: aRi = x;

            then

             A20: (the addF of F . (a,x)) <> x by A18, Def2;

            (a + u) = (( addR (x,o)) . (a1,u1)) by Def8

            .= ( addR (a1,u1)) by Def5

            .= (the addF of F . (aR,aRi)) by A16, A19, A20, Def4

            .= ( 0. ( ExField (x,o))) by A18, Def8;

            hence a is right_complementable by ALGSTR_0:def 11;

          end;

            suppose aRi <> x;

            then not aRi in {x} by TARSKI:def 1;

            then aRi in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider a1i = aRi as Element of C by XBOOLE_0:def 3;

            reconsider b = a1i as Element of ( ExField (x,o)) by Def8;



             A21: (the addF of F . (a,b)) <> x by A18, Def2;



             A22: aR <> o & aRi <> o by a1;

            (a + b) = (( addR (x,o)) . (a1,aRi)) by Def8

            .= ( addR (a1,a1i)) by Def5

            .= (the addF of F . (aR,aRi)) by A21, A22, Def4

            .= ( 0. ( ExField (x,o))) by A18, Def8;

            hence a is right_complementable by ALGSTR_0:def 11;

          end;

        end;

      end;

      hence ( ExField (x,o)) is right_complementable by ALGSTR_0:def 16;

    end;

    theorem :: FIELD_3:8



     Th8: for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( ExField (x,o)) is add-associative

    proof

      let x be non trivial Element of F, o be object;

      assume

       a1: not o in ( [#] F);

      then

       A1: a <> o;

      set C = ( carr (x,o)), E = ( ExField (x,o));

      set ADDR = the addF of F;



       A2: ( [#] E) = C by Def8;

      now

        let a,b,c be Element of E;

        per cases ;

          suppose

           A3: a = o;

          then a in {o} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of C by XBOOLE_0:def 3;

          per cases ;

            suppose

             A4: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of C by XBOOLE_0:def 3;

            per cases ;

              suppose

               A5: (ADDR . (x,x)) <> x;



               A6: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= (x + x) by A3, A4, A5, Def4;

               not (x + x) in {x} by A5, TARSKI:def 1;

              then (x + x) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

              then

              reconsider xx = (x + x) as Element of C by XBOOLE_0:def 3;



               A7: xx <> o by a1;

              per cases ;

                suppose

                 A8: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A9: ((a + b) + c) = (( addR (x,o)) . ((a + b),c1)) by Def8

                .= ( addR (xx,c1)) by A6, Def5;



                 A10: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (x + x) by A4, A5, A8, Def4;

                per cases ;

                  suppose

                   A11: (ADDR . (xx,x)) <> x;



                   A12: (ADDR . (x,xx)) = (x + (x + x))

                  .= ((x + x) + x);



                  thus ((a + b) + c) = ((x + x) + x) by A1, A8, A9, A11, Def4

                  .= ( addR (a1,xx)) by A1, A3, A11, A12, Def4

                  .= (( addR (x,o)) . (a1,xx)) by Def5

                  .= (a + (b + c)) by A10, Def8;

                end;

                  suppose

                   A13: (ADDR . (xx,x)) = x;



                   A14: (ADDR . (x,xx)) = (x + (x + x))

                  .= ((x + x) + x);



                  thus ((a + b) + c) = o by A7, A8, A9, A13, Def4

                  .= ( addR (a1,xx)) by A3, A7, A13, A14, Def4

                  .= (( addR (x,o)) . (a1,xx)) by Def5

                  .= (a + (b + c)) by A10, Def8;

                end;

              end;

                suppose

                 A15: c <> o;

                then not c in {o} by TARSKI:def 1;

                then c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;



                 A16: ((a + b) + c) = (( addR (x,o)) . ((a + b),c1)) by Def8

                .= ( addR (xx,c1)) by A6, Def5;



                 A17: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5;

                then

                reconsider bc = (b + c) as Element of C;

                per cases ;

                  suppose

                   A18: (ADDR . (x,c1)) <> x;

                  then

                   A19: (b + c) = (x + cR) by A4, A15, A17, Def4;

                  then

                   A20: (b + c) <> o by a1;

                  per cases ;

                    suppose (ADDR . (xx,c1)) <> x;



                    then

                     A21: ((a + b) + c) = ((x + x) + cR) by A7, A15, A16, Def4

                    .= (x + (x + cR)) by RLVECT_1:def 3

                    .= (ADDR . (x,(b + c))) by A4, A15, A17, A18, Def4;

                    per cases ;

                      suppose (ADDR . (x,bc)) <> x;



                      hence ((a + b) + c) = ( addR (a1,bc)) by A1, A3, A19, A21, Def4

                      .= (( addR (x,o)) . (a1,(b + c))) by Def5

                      .= (a + (b + c)) by Def8;

                    end;

                      suppose

                       A22: (ADDR . (x,bc)) = x;



                       A23: (ADDR . (x,bc)) = (x + (x + cR)) by A4, A15, A17, A18, Def4

                      .= ((x + x) + cR) by RLVECT_1:def 3

                      .= (ADDR . (xx,c1));



                      thus ((a + b) + c) = o by A7, A15, A16, A22, A23, Def4

                      .= ( addR (a1,bc)) by A3, A20, A22, Def4

                      .= (( addR (x,o)) . (a1,(b + c))) by Def5

                      .= (a + (b + c)) by Def8;

                    end;

                  end;

                    suppose

                     A24: (ADDR . (xx,c1)) = x;

                    then

                     A25: ((a + b) + c) = o by A7, A15, A16, Def4;

                    per cases ;

                      suppose (ADDR . (x,bc)) <> x;



                       A26: (ADDR . (x,bc)) = (x + (x + cR)) by A4, A15, A17, A18, Def4

                      .= ((x + x) + cR) by RLVECT_1:def 3

                      .= (ADDR . (xx,c1));



                      thus ((a + b) + c) = ( addR (a1,bc)) by A3, A20, A26, A24, A25, Def4

                      .= (( addR (x,o)) . (a1,(b + c))) by Def5

                      .= (a + (b + c)) by Def8;

                    end;

                      suppose

                       A27: (ADDR . (x,bc)) = x;

                      (ADDR . (x,bc)) = (x + (x + cR)) by A4, A15, A17, A18, Def4

                      .= ((x + x) + cR) by RLVECT_1:def 3

                      .= (ADDR . (xx,c1));



                      hence ((a + b) + c) = o by A7, A15, A16, A27, Def4

                      .= ( addR (a1,bc)) by A3, A20, A27, Def4

                      .= (( addR (x,o)) . (a1,(b + c))) by Def5

                      .= (a + (b + c)) by Def8;

                    end;

                  end;

                end;

                  suppose

                   A29: (ADDR . (x,c1)) = x;

                  then (x + cR) = x;

                  then

                   A30: c1 = ( 0. F) by RLVECT_1: 9;



                   A31: (b + c) = o by A4, A29, A15, A17, Def4;

                  per cases ;

                    suppose (ADDR . (xx,c1)) <> x;



                    hence ((a + b) + c) = ((x + x) + cR) by A7, A15, A16, Def4

                    .= ( addR (a1,bc)) by A3, A5, A30, A31, Def4

                    .= (( addR (x,o)) . (a1,(b + c))) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose (ADDR . (xx,c1)) = x;



                    then x = ((x + x) + cR)

                    .= (x + x) by A30;

                    hence ((a + b) + c) = (a + (b + c)) by A5;

                  end;

                end;

              end;

            end;

              suppose

               A33: (ADDR . (x,x)) = x;



               A34: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= o by A3, A4, A33, Def4;

              then (a + b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a + b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose c = o;

                hence ((a + b) + c) = (a + (b + c)) by A3;

              end;

                suppose

                 A36: c <> o;

                then not c in {o} by TARSKI:def 1;

                then c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;

                per cases ;

                  suppose

                   A37: (ADDR . (x,c1)) = x;



                   A38: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A4, A36, A37, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= o by A36, A34, A37, Def4

                  .= ( addR (a1,bc)) by A3, A33, A38, Def4

                  .= (( addR (x,o)) . (a1,(b + c))) by Def5

                  .= (a + (b + c)) by Def8;

                end;

                  suppose

                   A39: (ADDR . (x,c1)) <> x;



                   A40: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (x + cR) by A4, A36, A39, Def4;

                  reconsider bc = (b + c) as Element of C by Def8;



                   A41: ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= (ADDR . (x,c1)) by A34, A36, A39, Def4;

                  ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= ((x + x) + cR) by A33, A34, A36, A39, Def4

                  .= (x + (x + cR)) by RLVECT_1:def 3

                  .= (ADDR . (x,bc)) by A40;



                  hence ((a + b) + c) = ( addR (a1,bc)) by A1, A3, A39, A40, A41, Def4

                  .= (( addR (x,o)) . (a1,(b + c))) by Def5

                  .= (a + (b + c)) by Def8;

                end;

              end;

            end;

          end;

            suppose

             A42: b <> o;

            then not b in {o} by TARSKI:def 1;

            then b in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

            then

            reconsider bR = b as Element of F;

            reconsider b1 = b as Element of C by Def8;



             A43: (ADDR . (x,b)) = (x + bR)

            .= (bR + x)

            .= (ADDR . (b,x));

            per cases ;

              suppose

               A44: (ADDR . (x,b)) <> x;



               A45: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= (x + bR) by A3, A42, A44, Def4;

              then

               A46: (a + b) <> o by A1;

              then not (a + b) in {o} by TARSKI:def 1;

              then (a + b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              then

              reconsider abR = (a + b) as Element of F;

              reconsider ab = (a + b) as Element of C by Def8;

              per cases ;

                suppose

                 A47: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A48: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (bR + x) by A42, A43, A44, A47, Def4;



                 A49: (b + c) <> o by A1, A48;

                then not (b + c) in {o} by TARSKI:def 1;

                then (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider bcR = (b + c) as Element of F;

                reconsider bc = (b + c) as Element of C by Def8;



                 A50: (ADDR . (ab,x)) = ((x + bR) + x) by A45

                .= (x + (bR + x));

                per cases ;

                  suppose

                   A51: (ADDR . (ab,x)) <> x;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= (ADDR . (x,bc)) by A1, A3, A47, A48, A50, A51, Def4

                  .= ( addR (a1,bc)) by A1, A3, A48, A50, A51, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

                  suppose

                   A52: (ADDR . (ab,x)) = x;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= o by A46, A47, A52, Def4

                  .= ( addR (a1,bc)) by A3, A48, A49, A50, A52, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

              end;

                suppose

                 A53: c <> o;

                then not c in {o} by TARSKI:def 1;

                then c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;



                 A54: (ADDR . (ab,c)) = ((x + bR) + cR) by A45

                .= (x + (bR + cR)) by RLVECT_1:def 3;

                per cases ;

                  suppose

                   A55: (ADDR . (b,c)) <> x;



                   A56: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A42, A53, A55, Def4;



                   A57: (b + c) <> o by A1, A56;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  then

                  reconsider bcR = (b + c) as Element of F;

                  reconsider bc = (b + c) as Element of C by Def8;

                  per cases ;

                    suppose

                     A58: (ADDR . (ab,c1)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((x + bR) + cR) by A45, A58, A53, A46, Def4

                    .= (x + (bR + cR)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A1, A3, A54, A58, A56, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A59: (ADDR . (ab,c1)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A59, A53, A46, Def4

                    .= ( addR (a1,bc)) by A3, A54, A59, A56, A57, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A60: (ADDR . (b,c)) = x;



                   A61: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A60, A53, A42, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A62: (ADDR . (ab,c1)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((x + bR) + cR) by A45, A46, A53, A62, Def4

                    .= (x + (bR + cR)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A60, A3, A54, A62, A61, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A63: (ADDR . (ab,c1)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A63, A53, A46, Def4

                    .= ( addR (a1,bc)) by A60, A3, A54, A63, A61, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

              end;

            end;

              suppose

               A64: (ADDR . (x,b)) = x;



               A65: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= o by A64, A42, A3, Def4;

              then (a + b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a + b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose c = o;

                hence ((a + b) + c) = (a + (b + c)) by A3;

              end;

                suppose

                 A68: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A69: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;

                 A70:

                now

                  assume (ADDR . (b,c)) = x;



                  then (bR + cR) = (x + bR) by A64

                  .= (bR + x);

                  then x = cR by ALGSTR_0:def 4;

                  then c in {x} by TARSKI:def 1;

                  hence contradiction by A69, XBOOLE_0:def 5;

                end;



                 A72: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (bR + cR) by A70, A68, A42, Def4;



                 A73: (b + c) <> o by A72, A1;

                then not (b + c) in {o} by TARSKI:def 1;

                then (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider bcR = (b + c) as Element of F;

                reconsider bc = (b + c) as Element of C by Def8;



                 A74: (x + (bR + cR)) = ((x + bR) + cR) by RLVECT_1:def 3

                .= (x + cR) by A64;

                per cases ;

                  suppose

                   A75: (ADDR . (x,c1)) <> x;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= (ADDR . (x,c1)) by A65, A75, A68, Def4

                  .= ( addR (a1,bc)) by A74, A3, A75, A72, A1, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

                  suppose

                   A76: (ADDR . (x,c1)) = x;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= o by A76, A68, A65, Def4

                  .= ( addR (a1,bc)) by A73, A76, A74, A3, A72, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

              end;

            end;

          end;

        end;

          suppose

           A77: a <> o;

           not a in {o} by A77, TARSKI:def 1;

          then

           A78: a in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

          then

          reconsider aR = a as Element of F;

          reconsider a1 = a as Element of C by Def8;

          per cases ;

            suppose

             A79: b = o;

            b in {o} by A79, TARSKI:def 1;

            then

            reconsider b1 = b as Element of C by XBOOLE_0:def 3;

            per cases ;

              suppose

               A80: (ADDR . (a1,x)) = x;



               A81: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= o by A80, A79, A77, Def4;

              then (a + b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a + b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose

                 A81a: c = o;

                c in {o} by A81a, TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A82: (ADDR . (x,x)) = x;



                   A83: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A81a, A79, A82, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= o by A81, A81a, A82, Def4

                  .= ( addR (a1,bc)) by A80, A77, A83, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

                  suppose

                   A84: (ADDR . (x,x)) <> x;



                   A85: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (x + x) by A84, A79, A81a, Def4;

                  then

                   A86: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A87: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bcR = (b + c) as Element of F by A87;

                  reconsider bc = (b + c) as Element of C by Def8;



                   A88: ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= ((aR + x) + x) by A80, A81, A81a, A84, Def4;

                  now

                    assume (ADDR . (a1,bc)) = x;

                    then (aR + bcR) = (aR + x) by A80;

                    then bcR = x by ALGSTR_0:def 4;

                    then (b + c) in {x} by TARSKI:def 1;

                    hence contradiction by A87, XBOOLE_0:def 5;

                  end;



                  then (ADDR . (a1,bc)) = ( addR (a1,bc)) by A77, A86, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;



                  hence (a + (b + c)) = (aR + (x + x)) by A85

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

                end;

              end;

                suppose

                 A90: c <> o;

                 not c in {o} by A90, TARSKI:def 1;

                then

                 A91: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A91;

                per cases ;

                  suppose

                   A92: (ADDR . (x,c)) = x;



                   A93: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A92, A90, A79, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= o by A81, A90, A92, Def4

                  .= ( addR (a1,bc)) by A80, A77, A93, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

                  suppose

                   A94: (ADDR . (x,c)) <> x;



                   A95: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (x + cR) by A94, A90, A79, Def4;

                  then

                   A96: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A97: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A97;

                   A98:

                  now

                    assume (ADDR . (a1,bc)) = x;

                    then (aR + bcR) = (aR + x) by A80;

                    then bcR = x by ALGSTR_0:def 4;

                    then (b + c) in {x} by TARSKI:def 1;

                    hence contradiction by A97, XBOOLE_0:def 5;

                  end;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= ((aR + x) + cR) by A80, A81, A90, A94, Def4

                  .= (aR + (x + cR)) by RLVECT_1:def 3

                  .= ( addR (a1,bc)) by A98, A96, A77, A95, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

              end;

            end;

              suppose

               A100: (ADDR . (a1,x)) <> x;



               A101: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= (aR + x) by A79, A77, A100, Def4;

              then

               A102: (a + b) <> o by A1;

              then not (a + b) in {o} by TARSKI:def 1;

              then

               A103: (a + b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider ab = (a + b) as Element of C by Def8;

              reconsider abR = (a + b) as Element of F by A103;

              per cases ;

                suppose

                 A104: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A105: (ADDR . (x,x)) = x;



                   A106: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A105, A104, A79, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;

                   A107:

                  now

                    assume (ADDR . (ab,x)) = x;



                    then x = ((aR + x) + x) by A101

                    .= (aR + (x + x)) by RLVECT_1:def 3

                    .= (aR + x) by A105;

                    hence contradiction by A100;

                  end;



                  thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                  .= ( addR (ab,c1)) by Def5

                  .= ((aR + x) + x) by A101, A1, A104, A107, Def4

                  .= (aR + (x + x)) by RLVECT_1:def 3

                  .= ( addR (a1,bc)) by A105, A100, A77, A106, Def4

                  .= (( addR (x,o)) . (a,bc)) by Def5

                  .= (a + (b + c)) by Def8;

                end;

                  suppose

                   A109: (ADDR . (x,x)) <> x;



                   A110: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (x + x) by A109, A104, A79, Def4;

                  then

                   A111: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A112: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A112;



                   A113: (ADDR . (a,bc)) = (aR + (x + x)) by A110

                  .= ((aR + x) + x) by RLVECT_1:def 3

                  .= (ADDR . (ab,x)) by A101;

                  per cases ;

                    suppose

                     A114: (ADDR . (ab,x)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A102, A104, A114, Def4

                    .= ( addR (a1,bc)) by A114, A77, A113, A111, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A115: (ADDR . (ab,x)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= (ADDR . (ab,x)) by A101, A1, A104, A115, Def4

                    .= ( addR (a1,bc)) by A115, A77, A113, A111, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

              end;

                suppose

                 A116: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A117: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A117;

                per cases ;

                  suppose

                   A118: (ADDR . (x,c)) = x;



                   A119: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A118, A116, A79, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                   A120: (ADDR . (ab,c)) = ((aR + x) + cR) by A101

                  .= (aR + (x + cR)) by RLVECT_1:def 3

                  .= (ADDR . (a,x)) by A118;

                  per cases ;

                    suppose

                     A121: (ADDR . (ab,c1)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A102, A116, A121, Def4

                    .= ( addR (a1,bc)) by A121, A77, A119, A120, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A122: (ADDR . (ab,c1)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + x) + cR) by A101, A102, A116, A122, Def4

                    .= (aR + (x + cR)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A119, A100, A77, A118, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A123: (ADDR . (x,c)) <> x;



                   A124: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (x + cR) by A123, A116, A79, Def4;

                  then

                   A125: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A126: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A126;



                   A127: (ADDR . (a,bc)) = (aR + (x + cR)) by A124

                  .= ((aR + x) + cR) by RLVECT_1:def 3

                  .= (ADDR . (ab,c)) by A101;

                  per cases ;

                    suppose

                     A128: (ADDR . (ab,c1)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A102, A116, A128, Def4

                    .= ( addR (a1,bc)) by A128, A77, A125, A127, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A129: (the addF of F . (ab,c1)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + x) + cR) by A101, A102, A116, A129, Def4

                    .= (aR + (x + cR)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A129, A77, A124, A127, A125, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

              end;

            end;

          end;

            suppose

             A130: b <> o;

            then not b in {o} by TARSKI:def 1;

            then

             A131: b in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

            reconsider b1 = b as Element of C by Def8;

            reconsider bR = b as Element of F by A131;

             A132:

            now

              assume x = (x + x);

              then x = ( 0. F) by RLVECT_1: 9;

              hence contradiction by Def2;

            end;

            per cases ;

              suppose

               A134: (ADDR . (a,b)) = x;



               A135: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= o by A134, A130, A77, Def4;

              then (a + b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a + b) as Element of C by XBOOLE_0:def 3;

               A136:

              now

                assume (bR + x) = x;



                then

                 A138: (bR + x) = (aR + bR) by A134

                .= (bR + aR);

                x = aR by A138, ALGSTR_0:def 4;

                then a in {x} by TARSKI:def 1;

                hence contradiction by A78, XBOOLE_0:def 5;

              end;

              per cases ;

                suppose

                 A139: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A140: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (bR + x) by A136, A139, A130, Def4;

                then

                 A141: (b + c) <> o by A1;

                then not (b + c) in {o} by TARSKI:def 1;

                then

                 A142: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider bc = (b + c) as Element of C by Def8;

                reconsider bcR = (b + c) as Element of F by A142;

                 A143:

                now

                  assume (ADDR . (a,bc)) = x;



                  then x = (aR + (bR + x)) by A140

                  .= ((aR + bR) + x) by RLVECT_1:def 3

                  .= (x + x) by A134;

                  hence contradiction by A132;

                end;



                thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                .= ( addR (ab,c1)) by Def5

                .= ((aR + bR) + x) by A134, A135, A139, A132, Def4

                .= (aR + (bR + x)) by RLVECT_1:def 3

                .= ( addR (a1,bc)) by A77, A141, A140, A143, Def4

                .= (( addR (x,o)) . (a,bc)) by Def5

                .= (a + (b + c)) by Def8;

              end;

                suppose

                 A145: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A146: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A146;

                per cases ;

                  suppose

                   A147: (ADDR . (b,c)) <> x;



                   A148: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A145, A130, A147, Def4;

                  then

                   A149: (b + c) <> o by A1;

                   not (b + c) in {o} by A149, TARSKI:def 1;

                  then

                   A150: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A150;

                  per cases ;

                    suppose

                     A151: (ADDR . (x,c)) <> x;

                     A152:

                    now

                      assume (ADDR . (a,bc)) = x;



                      then x = (aR + (bR + cR)) by A148

                      .= ((aR + bR) + cR) by RLVECT_1:def 3

                      .= (x + cR) by A134;

                      hence contradiction by A151;

                    end;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + bR) + cR) by A134, A135, A145, A151, Def4

                    .= (aR + (bR + cR)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A77, A148, A149, A152, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A154: (ADDR . (x,c)) = x;



                     A155: (aR + (bR + cR)) = ((aR + bR) + cR) by RLVECT_1:def 3

                    .= x by A134, A154;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A154, A135, A145, Def4

                    .= ( addR (a1,bc)) by A155, A77, A149, A148, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A156: (ADDR . (b,c)) = x;



                  then

                   A157: (bR + cR) = (aR + bR) by A134

                  .= (bR + aR);



                   A158: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A130, A145, A156, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                   A159: (x + cR) = (aR + x) by A157, ALGSTR_0:def 4

                  .= (ADDR . (a,x));

                  per cases ;

                    suppose

                     A160: (ADDR . (x,c)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= (x + cR) by A135, A145, A160, Def4

                    .= ( addR (a1,bc)) by A77, A159, A160, A158, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A161: (ADDR . (x,c)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A135, A145, A161, Def4

                    .= ( addR (a1,bc)) by A77, A159, A161, A158, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

              end;

            end;

              suppose

               A162: (ADDR . (a,b)) <> x;



               A163: (a + b) = (( addR (x,o)) . (a1,b1)) by Def8

              .= ( addR (a1,b1)) by Def5

              .= (aR + bR) by A162, A130, A77, Def4;

              then

               A164: (a + b) <> o by A1;

              then not (a + b) in {o} by TARSKI:def 1;

              then

               A165: (a + b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider ab = (a + b) as Element of C by Def8;

              reconsider abR = (a + b) as Element of F by A165;

              per cases ;

                suppose

                 A166: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A167: (ADDR . (b,x)) <> x;



                   A168: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + x) by A166, A130, A167, Def4;

                  then

                   A169: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A170: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A170;



                   A171: (ADDR . (ab,x)) = ((aR + bR) + x) by A163

                  .= (aR + (bR + x)) by RLVECT_1:def 3

                  .= (the addF of F . (a,bc)) by A168;

                  per cases ;

                    suppose

                     A172: (ADDR . (ab,x)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + bR) + x) by A1, A163, A166, A172, Def4

                    .= (aR + (bR + x)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A77, A168, A169, A171, A172, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A173: (ADDR . (ab,x)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A164, A166, A173, Def4

                    .= ( addR (a1,bc)) by A77, A173, A169, A171, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A174: (ADDR . (b,x)) = x;



                   A175: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A166, A130, A174, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                   A176: ((aR + bR) + x) = (aR + (bR + x)) by RLVECT_1:def 3

                  .= (the addF of F . (a,x)) by A174;

                  per cases ;

                    suppose

                     A177: (ADDR . (ab,x)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + bR) + x) by A163, A1, A166, A177, Def4

                    .= ( addR (a1,bc)) by A163, A77, A177, A175, A176, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A178: (ADDR . (ab,x)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A164, A166, A178, Def4

                    .= ( addR (a1,bc)) by A163, A77, A178, A175, A176, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

              end;

                suppose

                 A179: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A180: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A180;

                per cases ;

                  suppose

                   A181: (ADDR . (b,c)) <> x;



                   A182: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A179, A130, A181, Def4;

                  then

                   A183: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A184: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A184;



                   A185: (ADDR . (ab,c)) = ((aR + bR) + cR) by A163

                  .= (aR + (bR + cR)) by RLVECT_1:def 3

                  .= (ADDR . (a,bc)) by A182;

                  per cases ;

                    suppose

                     A186: (ADDR . (ab,c)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + bR) + cR) by A163, A164, A179, A186, Def4

                    .= (aR + (bR + cR)) by RLVECT_1:def 3

                    .= ( addR (a1,bc)) by A183, A77, A186, A182, A185, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A187: (ADDR . (ab,c)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A164, A179, A187, Def4

                    .= ( addR (a1,bc)) by A183, A77, A187, A185, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A188: (ADDR . (b,c)) = x;



                   A189: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A130, A179, A188, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b + c) as Element of C by XBOOLE_0:def 3;



                   A190: ((aR + bR) + cR) = (aR + (bR + cR)) by RLVECT_1:def 3

                  .= (ADDR . (a,x)) by A188;

                  per cases ;

                    suppose

                     A191: (ADDR . (ab,c)) <> x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= ((aR + bR) + cR) by A163, A164, A179, A191, Def4

                    .= ( addR (a1,bc)) by A77, A163, A189, A190, A191, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                    suppose

                     A192: (ADDR . (ab,c)) = x;



                    thus ((a + b) + c) = (( addR (x,o)) . (ab,c1)) by Def8

                    .= ( addR (ab,c1)) by Def5

                    .= o by A164, A179, A192, Def4

                    .= ( addR (a1,bc)) by A163, A77, A192, A189, A190, Def4

                    .= (( addR (x,o)) . (a,bc)) by Def5

                    .= (a + (b + c)) by Def8;

                  end;

                end;

              end;

            end;

          end;

        end;

      end;

      hence ( ExField (x,o)) is add-associative by RLVECT_1:def 3;

    end;

    registration

      let F be non almost_trivial Field;

      let x be non trivial Element of F;

      let o be object;

      cluster ( ExField (x,o)) -> commutative;

      coherence

      proof



         A1: ( [#] ( ExField (x,o))) = ( carr (x,o)) by Def8;

        now

          let a,b be Element of ( ExField (x,o));

          per cases ;

            suppose

             A2: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of ( carr (x,o)) by XBOOLE_0:def 3;

            per cases ;

              suppose

               A3: a = o;

              then a in {o} by TARSKI:def 1;

              then

              reconsider a1 = a as Element of ( carr (x,o)) by XBOOLE_0:def 3;

              thus (a * b) = (b * a) by A3, A2;

            end;

              suppose

               A4: a <> o;

              then not a in {o} by TARSKI:def 1;

              then

               A5: a in (( [#] F) \ {x}) by A1, XBOOLE_0:def 3;

              reconsider a1 = a as Element of ( carr (x,o)) by Def8;

              reconsider aR = a as Element of F by A5;



               A6: (the multF of F . (a1,x)) = (aR * x)

              .= (x * aR) by GROUP_1:def 12

              .= (the multF of F . (x,a1));

              per cases ;

                suppose

                 A7: (the multF of F . (a,x)) <> x;



                thus (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

                .= ( multR (a1,b1)) by Def7

                .= (the multF of F . (a,x)) by A7, A4, A2, Def6

                .= ( multR (b1,a1)) by A6, A7, A4, A2, Def6

                .= (( multR (x,o)) . (b1,a1)) by Def7

                .= (b * a) by Def8;

              end;

                suppose

                 A8: (the multF of F . (a,x)) = x;



                thus (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

                .= ( multR (a1,b1)) by Def7

                .= o by A8, A4, A2, Def6

                .= ( multR (b1,a1)) by A6, A8, A4, A2, Def6

                .= (( multR (x,o)) . (b1,a1)) by Def7

                .= (b * a) by Def8;

              end;

            end;

          end;

            suppose

             A9: b <> o;

            then not b in {o} by TARSKI:def 1;

            then

             A10: b in (( [#] F) \ {x}) by A1, XBOOLE_0:def 3;

            reconsider b1 = b as Element of ( carr (x,o)) by Def8;

            per cases ;

              suppose

               A11: a = o;

              then a in {o} by TARSKI:def 1;

              then

              reconsider a1 = a as Element of ( carr (x,o)) by XBOOLE_0:def 3;

              reconsider bR = b as Element of F by A10;



               A12: (the multF of F . (x,b1)) = (x * bR)

              .= (bR * x) by GROUP_1:def 12

              .= (the multF of F . (b1,x));

              per cases ;

                suppose

                 A13: (the multF of F . (x,b)) <> x;



                thus (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

                .= ( multR (a1,b1)) by Def7

                .= (the multF of F . (x,b)) by A13, A11, A9, Def6

                .= ( multR (b1,a1)) by A12, A13, A11, A9, Def6

                .= (( multR (x,o)) . (b1,a1)) by Def7

                .= (b * a) by Def8;

              end;

                suppose

                 A14: (the multF of F . (x,b)) = x;



                thus (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

                .= ( multR (a1,b1)) by Def7

                .= o by A14, A11, A9, Def6

                .= ( multR (b1,a1)) by A12, A14, A11, A9, Def6

                .= (( multR (x,o)) . (b1,a1)) by Def7

                .= (b * a) by Def8;

              end;

            end;

              suppose

               A15: a <> o;

              then not a in {o} by TARSKI:def 1;

              then

               A16: a in (( [#] F) \ {x}) by A1, XBOOLE_0:def 3;

              reconsider a1 = a as Element of ( carr (x,o)) by Def8;

              reconsider aR = a, bR = b as Element of ( [#] F) by A10, A16;



               A17: (the multF of F . (a,b)) = (aR * bR)

              .= (bR * aR) by GROUP_1:def 12

              .= (the multF of F . (b,a));

              per cases ;

                suppose

                 A18: (the multF of F . (a,b)) <> x;



                thus (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

                .= ( multR (a1,b1)) by Def7

                .= (the multF of F . (a,b)) by A18, A15, A9, Def6

                .= ( multR (b1,a1)) by A17, A18, A15, A9, Def6

                .= (( multR (x,o)) . (b1,a1)) by Def7

                .= (b * a) by Def8;

              end;

                suppose

                 A19: (the multF of F . (a,b)) = x;



                thus (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

                .= ( multR (a1,b1)) by Def7

                .= o by A19, A15, A9, Def6

                .= ( multR (b1,a1)) by A17, A19, A15, A9, Def6

                .= (( multR (x,o)) . (b1,a1)) by Def7

                .= (b * a) by Def8;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_3:9



     Th9: for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( ExField (x,o)) is well-unital

    proof

      let x be non trivial Element of F;

      let u be object;

      assume not u in ( [#] F);

      then

       A1: for a be Element of F holds a <> u;

      set C = ( carr (x,u));

      set E = ( ExField (x,u));



       A2: ( [#] E) = C by Def8;

      now

        let a be Element of E;



         A3: ( 1. E) = ( 1. F) by Def8;

        ( 1. F) <> x by Def2;

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

        then ( 1. F) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

        then

        reconsider o = ( 1. F) as Element of C by XBOOLE_0:def 3;



         A4: o <> u by A1;

        per cases ;

          suppose

           A5: a = u;

          then a in {u} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of C by XBOOLE_0:def 3;



           A6: (the multF of F . (x,( 1. F))) = (x * ( 1. F))

          .= x;



          thus (a * ( 1. E)) = (( multR (x,u)) . (a1,o)) by A3, Def8

          .= ( multR (a1,o)) by Def7

          .= a by A6, A4, A5, Def6;



           A7: (the multF of F . (( 1. F),x)) = (( 1. F) * x)

          .= x;



          thus (( 1. E) * a) = (( multR (x,u)) . (o,a1)) by A3, Def8

          .= ( multR (o,a1)) by Def7

          .= a by A7, A4, A5, Def6;

        end;

          suppose

           A8: a <> u;

          then not a in {u} by TARSKI:def 1;

          then

           A9: a in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

          reconsider a1 = a as Element of C by Def8;

          reconsider aR = a as Element of ( [#] F) by A9;



           A10: (the multF of F . (a,o)) = (aR * ( 1. F))

          .= aR;



           A11: not aR in {x} by A9, XBOOLE_0:def 5;

          then

           A12: (the multF of F . (a,o)) <> x by A10, TARSKI:def 1;



          thus (a * ( 1. E)) = (( multR (x,u)) . (a1,o)) by A3, Def8

          .= ( multR (a1,o)) by Def7

          .= (aR * ( 1. F)) by A12, A4, A8, Def6

          .= a;

          (the multF of F . (o,a)) = (( 1. F) * aR)

          .= aR;

          then

           A13: (the multF of F . (o,a)) <> x by A11, TARSKI:def 1;



          thus (( 1. E) * a) = (( multR (x,u)) . (o,a1)) by A3, Def8

          .= ( multR (o,a1)) by Def7

          .= (( 1. F) * aR) by A13, A4, A8, Def6

          .= a;

        end;

      end;

      hence ( ExField (x,u)) is well-unital;

    end;

    theorem :: FIELD_3:10



     Th10: for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( ExField (x,o)) is associative

    proof

      let x be non trivial Element of F;

      let o be object;

      assume not o in ( [#] F);

      then

       A1: a <> o;

      set C = ( carr (x,o)), E = ( ExField (x,o));

      set MULTR = the multF of F;



       A2: ( [#] E) = C by Def8;

      now

        let a,b,c be Element of E;

        per cases ;

          suppose

           A3: a = o;

          then a in {o} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of C by XBOOLE_0:def 3;

          per cases ;

            suppose

             A4: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of C by XBOOLE_0:def 3;

            per cases ;

              suppose

               A5: (MULTR . (x,x)) <> x;



               A6: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (x * x) by A5, A4, A3, Def6;

               not (x * x) in {x} by A5, TARSKI:def 1;

              then (x * x) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

              then

              reconsider xx = (x * x) as Element of C by XBOOLE_0:def 3;



               A7: xx <> o by A1;

              per cases ;

                suppose

                 A8: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A9: ((a * b) * c) = (( multR (x,o)) . ((a * b),c1)) by Def8

                .= ( multR (xx,c1)) by A6, Def7;



                 A10: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7

                .= (x * x) by A4, A5, A8, Def6;



                 A11: (MULTR . (x,xx)) = (x * (x * x))

                .= ((x * x) * x) by GROUP_1:def 3;

                per cases ;

                  suppose

                   A12: (MULTR . (xx,x)) <> x;



                  hence ((a * b) * c) = ((x * x) * x) by A8, A1, A9, Def6

                  .= ( multR (a1,xx)) by A3, A11, A12, A1, Def6

                  .= (( multR (x,o)) . (a1,xx)) by Def7

                  .= (a * (b * c)) by A10, Def8;

                end;

                  suppose

                   A13: (MULTR . (xx,x)) = x;



                  hence ((a * b) * c) = o by A9, A7, A8, Def6

                  .= ( multR (a1,xx)) by A7, A11, A13, A3, Def6

                  .= (( multR (x,o)) . (a1,xx)) by Def7

                  .= (a * (b * c)) by A10, Def8;

                end;

              end;

                suppose

                 A14: c <> o;

                then not c in {o} by TARSKI:def 1;

                then c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;



                 A15: ((a * b) * c) = (( multR (x,o)) . ((a * b),c1)) by Def8

                .= ( multR (xx,c1)) by A6, Def7;



                 A16: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7;

                then

                reconsider bc = (b * c) as Element of C;

                per cases ;

                  suppose

                   A17: (MULTR . (x,c1)) <> x;

                  then

                   A18: (b * c) = (x * cR) by A16, A14, A4, Def6;

                  then

                   A19: (b * c) <> o by A1;

                  per cases ;

                    suppose (MULTR . (xx,c1)) <> x;



                    then

                     A20: ((a * b) * c) = ((x * x) * cR) by A7, A15, A14, Def6

                    .= (x * (x * cR)) by GROUP_1:def 3

                    .= (MULTR . (x,(b * c))) by A17, A16, A14, A4, Def6;

                    per cases ;

                      suppose (MULTR . (x,bc)) <> x;



                      hence ((a * b) * c) = ( multR (a1,bc)) by A18, A1, A3, Def6, A20

                      .= (( multR (x,o)) . (a1,(b * c))) by Def7

                      .= (a * (b * c)) by Def8;

                    end;

                      suppose

                       A21: (MULTR . (x,bc)) = x;



                       A22: (MULTR . (x,bc)) = (x * (x * cR)) by A17, A16, A14, A4, Def6

                      .= ((x * x) * cR) by GROUP_1:def 3

                      .= (MULTR . (xx,c1));



                      thus ((a * b) * c) = o by A15, A7, A14, A22, A21, Def6

                      .= ( multR (a1,bc)) by A3, A19, A21, Def6

                      .= (( multR (x,o)) . (a1,(b * c))) by Def7

                      .= (a * (b * c)) by Def8;

                    end;

                  end;

                    suppose

                     A23: (MULTR . (xx,c1)) = x;

                    then

                     A24: ((a * b) * c) = o by A7, A15, A14, Def6;

                    per cases ;

                      suppose (MULTR . (x,bc)) <> x;



                       A25: (MULTR . (x,bc)) = (x * (x * cR)) by A17, A16, A14, A4, Def6

                      .= ((x * x) * cR) by GROUP_1:def 3

                      .= (MULTR . (xx,c1));



                      thus ((a * b) * c) = ( multR (a1,bc)) by A25, A23, A19, A3, Def6, A24

                      .= (( multR (x,o)) . (a1,(b * c))) by Def7

                      .= (a * (b * c)) by Def8;

                    end;

                      suppose

                       A26: (MULTR . (x,bc)) = x;



                       A27: (MULTR . (x,bc)) = (x * (x * cR)) by A17, A16, A14, A4, Def6

                      .= ((x * x) * cR) by GROUP_1:def 3

                      .= (MULTR . (xx,c1));



                      thus ((a * b) * c) = o by A15, A7, A14, A27, A26, Def6

                      .= ( multR (a1,bc)) by A19, A26, A3, Def6

                      .= (( multR (x,o)) . (a1,(b * c))) by Def7

                      .= (a * (b * c)) by Def8;

                    end;

                  end;

                end;

                  suppose

                   A28: (MULTR . (x,c1)) = x;



                   A29: x <> ( 0. F) by Def2;



                   A30: x = (x * cR) by A28

                  .= (cR * x) by GROUP_1:def 12;



                   A31: cR = (cR * ( 1_ F))

                  .= (cR * (x * (x " ))) by A29, VECTSP_2: 9

                  .= (x * (x " )) by A30, GROUP_1:def 3

                  .= ( 1_ F) by A29, VECTSP_2: 9;



                   A32: (b * c) = o by A28, A16, A14, A4, Def6;

                  per cases ;

                    suppose (MULTR . (xx,c1)) <> x;



                    hence ((a * b) * c) = ((x * x) * cR) by A15, A7, A14, Def6

                    .= ( multR (a1,bc)) by A31, A32, A5, A3, Def6

                    .= (( multR (x,o)) . (a1,(b * c))) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose (MULTR . (xx,c1)) = x;



                    then x = ((x * x) * cR)

                    .= (x * x) by A31;

                    hence ((a * b) * c) = (a * (b * c)) by A5;

                  end;

                end;

              end;

            end;

              suppose

               A34: (MULTR . (x,x)) = x;



               A35: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A34, A4, A3, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a * b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose

                 A36: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A37: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7

                .= o by A34, A36, A4, Def6;

                then (b * c) in {o} by TARSKI:def 1;

                then

                reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;

                thus ((a * b) * c) = (a * (b * c)) by A35, A36, A37, A3;

              end;

                suppose

                 A38: c <> o;

                then not c in {o} by TARSKI:def 1;

                then c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;

                per cases ;

                  suppose

                   A39: (MULTR . (x,c1)) = x;



                   A40: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A39, A38, A4, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= o by A39, A35, A38, Def6

                  .= ( multR (a1,bc)) by A40, A34, A3, Def6

                  .= (( multR (x,o)) . (a1,(b * c))) by Def7

                  .= (a * (b * c)) by Def8;

                end;

                  suppose

                   A41: (MULTR . (x,c1)) <> x;



                   A42: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (x * cR) by A41, A38, A4, Def6;

                  then (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  then

                  reconsider bcR = (b * c) as Element of F;

                  reconsider bc = (b * c) as Element of C by Def8;



                   A43: ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= (MULTR . (x,c1)) by A35, A38, A41, Def6;

                  ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= ((x * x) * cR) by A34, A35, A38, A41, Def6

                  .= (x * (x * cR)) by GROUP_1:def 3

                  .= (MULTR . (x,bc)) by A42;



                  hence ((a * b) * c) = ( multR (a1,bc)) by A41, A43, A42, A1, A3, Def6

                  .= (( multR (x,o)) . (a1,(b * c))) by Def7

                  .= (a * (b * c)) by Def8;

                end;

              end;

            end;

          end;

            suppose

             A44: b <> o;

            then not b in {o} by TARSKI:def 1;

            then b in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

            then

            reconsider bR = b as Element of F;

            reconsider b1 = b as Element of C by Def8;



             A45: (MULTR . (x,b)) = (x * bR)

            .= (bR * x) by GROUP_1:def 12

            .= (MULTR . (b,x));

            per cases ;

              suppose

               A46: (MULTR . (x,b)) <> x;



               A47: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (x * bR) by A46, A44, A3, Def6;

              then

               A48: (a * b) <> o by A1;

              then not (a * b) in {o} by TARSKI:def 1;

              then (a * b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              then

              reconsider abR = (a * b) as Element of F;

              reconsider ab = (a * b) as Element of C by Def8;

              per cases ;

                suppose

                 A49: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A50: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7

                .= (bR * x) by A45, A46, A49, A44, Def6;

                then

                 A51: (b * c) <> o by A1;

                then not (b * c) in {o} by TARSKI:def 1;

                then (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider bcR = (b * c) as Element of F;

                reconsider bc = (b * c) as Element of C by Def8;



                 A52: (MULTR . (ab,x)) = ((x * bR) * x) by A47

                .= (x * (bR * x)) by GROUP_1:def 3;

                per cases ;

                  suppose

                   A53: (MULTR . (ab,x)) <> x;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= (MULTR . (ab,x)) by A47, A1, Def6, A49, A53

                  .= ( multR (a1,bc)) by A53, A52, A50, A1, A3, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

                  suppose

                   A54: (MULTR . (ab,x)) = x;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= o by A48, A49, A54, Def6

                  .= ( multR (a1,bc)) by A54, A52, A50, A51, A3, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

              end;

                suppose

                 A55: c <> o;

                then not c in {o} by TARSKI:def 1;

                then c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;



                 A56: (MULTR . (ab,c)) = ((x * bR) * cR) by A47

                .= (x * (bR * cR)) by GROUP_1:def 3;

                per cases ;

                  suppose

                   A57: (MULTR . (b,c)) <> x;



                   A58: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (bR * cR) by A57, A55, A44, Def6;

                  then

                   A59: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  then

                  reconsider bcR = (b * c) as Element of F;

                  reconsider bc = (b * c) as Element of C by Def8;

                  per cases ;

                    suppose

                     A60: (MULTR . (ab,c1)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((x * bR) * cR) by A47, A60, A55, A48, Def6

                    .= (x * (bR * cR)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A3, A56, A60, A58, A1, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A61: (MULTR . (ab,c1)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A61, A55, A48, Def6

                    .= ( multR (a1,bc)) by A3, A56, A61, A58, A59, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

                  suppose

                   A62: (MULTR . (b,c)) = x;



                   A63: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A62, A55, A44, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A64: (MULTR . (ab,c1)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((x * bR) * cR) by A47, A64, A55, A48, Def6

                    .= (x * (bR * cR)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A62, A3, A56, A64, A63, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A65: (MULTR . (ab,c1)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A65, A55, A48, Def6

                    .= ( multR (a1,bc)) by A62, A3, A56, A65, A63, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

              end;

            end;

              suppose

               A66: (MULTR . (x,b)) = x;



               A67: x <> ( 0. F) by Def2;



               A68: x = (x * bR) by A66

              .= (bR * x) by GROUP_1:def 12;



               A69: bR = (bR * ( 1_ F))

              .= (bR * (x * (x " ))) by A67, VECTSP_2: 9

              .= (x * (x " )) by A68, GROUP_1:def 3

              .= ( 1_ F) by A67, VECTSP_2: 9;



               A70: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A66, A44, A3, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a * b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose

                 A71: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A72: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7

                .= o by A45, A66, A71, A44, Def6;

                then (b * c) in {o} by TARSKI:def 1;

                then

                reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;

                thus ((a * b) * c) = (a * (b * c)) by A70, A71, A72, A3;

              end;

                suppose

                 A73: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A74: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider cR = c as Element of F;

                reconsider c1 = c as Element of C by Def8;



                 A75: bR <> ( 0. F) by A69;

                 A76:

                now

                  assume (MULTR . (b,c)) = x;



                  then (bR * cR) = (x * bR) by A66

                  .= (bR * x) by GROUP_1:def 12;

                  then cR = x by A75, ALGSTR_0:def 36, ALGSTR_0:def 20;

                  then c in {x} by TARSKI:def 1;

                  hence contradiction by A74, XBOOLE_0:def 5;

                end;



                 A78: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7

                .= (bR * cR) by A76, A73, A44, Def6;

                then

                 A79: (b * c) <> o by A1;

                then not (b * c) in {o} by TARSKI:def 1;

                then (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                then

                reconsider bcR = (b * c) as Element of F;

                reconsider bc = (b * c) as Element of C by Def8;



                 A80: (x * (bR * cR)) = ((x * bR) * cR) by GROUP_1:def 3

                .= (x * cR) by A66;

                per cases ;

                  suppose

                   A81: (MULTR . (x,c1)) <> x;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= (MULTR . (x,c1)) by A70, A81, A73, Def6

                  .= ( multR (a1,bc)) by A80, A3, A81, A78, A1, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

                  suppose

                   A82: (MULTR . (x,c1)) = x;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= o by A82, A73, A70, Def6

                  .= ( multR (a1,bc)) by A79, A82, A80, A3, A78, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

              end;

            end;

          end;

        end;

          suppose

           A83: a <> o;

          then not a in {o} by TARSKI:def 1;

          then

           A84: a in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

          then

          reconsider aR = a as Element of F;

          reconsider a1 = a as Element of C by Def8;

          per cases ;

            suppose

             A85: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of C by XBOOLE_0:def 3;

            per cases ;

              suppose

               A86: (MULTR . (a1,x)) = x;



               A87: x <> ( 0. F) by Def2;

              aR = (aR * ( 1_ F))

              .= (aR * (x * (x " ))) by A87, VECTSP_2: 9

              .= ((aR * x) * (x " )) by GROUP_1:def 3

              .= ( 1_ F) by A86, A87, VECTSP_2: 9;

              then

               A88: aR <> ( 0. F);



               A89: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A86, A85, A83, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a * b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose

                 A90: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A91: (MULTR . (x,x)) = x;



                   A92: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A90, A85, A91, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= o by A89, A90, A91, Def6

                  .= ( multR (a1,bc)) by A86, A83, A92, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

                  suppose

                   A93: (MULTR . (x,x)) <> x;



                   A94: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (x * x) by A93, A90, A85, Def6;

                  then

                   A95: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A96: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  then

                  reconsider bcR = (b * c) as Element of F;

                  reconsider bc = (b * c) as Element of C by Def8;



                   A97: ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= ((aR * x) * x) by A86, A89, A90, A93, Def6;

                  now

                    assume (MULTR . (a1,bc)) = x;

                    then (aR * bcR) = (aR * x) by A86;

                    then bcR = x by A88, ALGSTR_0:def 36, ALGSTR_0:def 20;

                    then (b * c) in {x} by TARSKI:def 1;

                    hence contradiction by A96, XBOOLE_0:def 5;

                  end;



                  then (MULTR . (a1,bc)) = ( multR (a1,bc)) by A83, A95, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;



                  hence (a * (b * c)) = (aR * (x * x)) by A94

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

                end;

              end;

                suppose

                 A99: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A100: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A100;

                per cases ;

                  suppose

                   A101: (MULTR . (x,c)) = x;



                   A102: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A101, A99, A85, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= o by A89, A99, A101, Def6

                  .= ( multR (a1,bc)) by A86, A83, A102, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

                  suppose

                   A103: (MULTR . (x,c)) <> x;



                   A104: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (x * cR) by A103, A99, A85, Def6;

                  then

                   A105: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A106: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b * c) as Element of C by Def8;

                  reconsider bcR = (b * c) as Element of F by A106;

                   A107:

                  now

                    assume (MULTR . (a1,bc)) = x;

                    then (aR * bcR) = (aR * x) by A86;

                    then bcR = x by A88, ALGSTR_0:def 36, ALGSTR_0:def 20;

                    then (b * c) in {x} by TARSKI:def 1;

                    hence contradiction by A106, XBOOLE_0:def 5;

                  end;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= ((aR * x) * cR) by A86, A89, A99, A103, Def6

                  .= (aR * (x * cR)) by GROUP_1:def 3

                  .= ( multR (a1,bc)) by A107, A105, A83, A104, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

              end;

            end;

              suppose

               A109: (MULTR . (a1,x)) <> x;



               A110: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (aR * x) by A85, A83, A109, Def6;

              then

               A111: (a * b) <> o by A1;

              then not (a * b) in {o} by TARSKI:def 1;

              then

               A112: (a * b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider ab = (a * b) as Element of C by Def8;

              reconsider abR = (a * b) as Element of F by A112;

              per cases ;

                suppose

                 A113: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A114: (MULTR . (x,x)) = x;



                   A115: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A114, A113, A85, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;

                   A116:

                  now

                    assume (MULTR . (ab,x)) = x;



                    then x = ((aR * x) * x) by A110

                    .= (aR * (x * x)) by GROUP_1:def 3

                    .= (aR * x) by A114;

                    hence contradiction by A109;

                  end;



                  thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                  .= ( multR (ab,c1)) by Def7

                  .= ((aR * x) * x) by A110, A1, A113, A116, Def6

                  .= (aR * (x * x)) by GROUP_1:def 3

                  .= ( multR (a1,bc)) by A114, A109, A83, A115, Def6

                  .= (( multR (x,o)) . (a,bc)) by Def7

                  .= (a * (b * c)) by Def8;

                end;

                  suppose

                   A118: (MULTR . (x,x)) <> x;



                   A119: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (x * x) by A118, A113, A85, Def6;

                  then

                   A120: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A121: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b * c) as Element of C by Def8;

                  reconsider bcR = (b * c) as Element of F by A121;



                   A122: (MULTR . (a,bc)) = (aR * (x * x)) by A119

                  .= ((aR * x) * x) by GROUP_1:def 3

                  .= (MULTR . (ab,x)) by A110;

                  per cases ;

                    suppose

                     A123: (MULTR . (ab,x)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A111, A113, A123, Def6

                    .= ( multR (a1,bc)) by A123, A83, A122, A120, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A124: (MULTR . (ab,x)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= (MULTR . (ab,x)) by A110, A1, A113, A124, Def6

                    .= ( multR (a1,bc)) by A124, A83, A122, A120, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

              end;

                suppose

                 A125: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A126: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A126;

                per cases ;

                  suppose

                   A127: (MULTR . (x,c)) = x;



                   A128: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A127, A125, A85, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                   A129: (MULTR . (ab,c)) = ((aR * x) * cR) by A110

                  .= (aR * (x * cR)) by GROUP_1:def 3

                  .= (MULTR . (a,x)) by A127;

                  per cases ;

                    suppose

                     A130: (MULTR . (ab,c1)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A111, A125, A130, Def6

                    .= ( multR (a1,bc)) by A130, A83, A128, A129, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A131: (MULTR . (ab,c1)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * x) * cR) by A110, A111, A125, A131, Def6

                    .= (aR * (x * cR)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A127, A109, A83, A128, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

                  suppose

                   A132: (MULTR . (x,c)) <> x;



                   A133: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (x * cR) by A132, A125, A85, Def6;

                  then

                   A134: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A135: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b * c) as Element of C by Def8;

                  reconsider bcR = (b * c) as Element of F by A135;



                   A136: (MULTR . (a,bc)) = (aR * (x * cR)) by A133

                  .= ((aR * x) * cR) by GROUP_1:def 3

                  .= (MULTR . (ab,c)) by A110;

                  per cases ;

                    suppose

                     A137: (MULTR . (ab,c1)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A111, A125, A137, Def6

                    .= ( multR (a1,bc)) by A137, A83, A136, A134, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A138: (MULTR . (ab,c1)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * x) * cR) by A110, A111, A125, A138, Def6

                    .= (aR * (x * cR)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A138, A83, A133, A136, A134, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

              end;

            end;

          end;

            suppose

             A139: b <> o;

            then not b in {o} by TARSKI:def 1;

            then

             A140: b in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

            reconsider b1 = b as Element of C by Def8;

            reconsider bR = b as Element of F by A140;

             A141:

            now

              assume

               A142: x = (x * x);

              x <> ( 0. F) by Def2;

              then

               A143: x is left_mult-cancelable by ALGSTR_0:def 36;

              (x * x) = (x * ( 1. F)) by A142;

              hence contradiction by A143, ALGSTR_0:def 20, Def2;

            end;

            per cases ;

              suppose

               A144: (MULTR . (a,b)) = x;



               A145: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A144, A139, A83, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab = (a * b) as Element of C by XBOOLE_0:def 3;

               A146:

              now

                assume bR = ( 0. F);

                then (aR * ( 0. F)) = x by A144;

                hence contradiction by Def2;

              end;

               A148:

              now

                assume (bR * x) = x;



                then (bR * x) = (aR * bR) by A144

                .= (bR * aR) by GROUP_1:def 12;

                then x = aR by A146, ALGSTR_0:def 36, ALGSTR_0:def 20;

                then a in {x} by TARSKI:def 1;

                hence contradiction by A84, XBOOLE_0:def 5;

              end;

              per cases ;

                suppose

                 A150: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A151: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                .= ( multR (b1,c1)) by Def7

                .= (bR * x) by A148, A150, A139, Def6;

                then

                 A152: (b * c) <> o by A1;

                then not (b * c) in {o} by TARSKI:def 1;

                then

                 A153: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider bc = (b * c) as Element of C by Def8;

                reconsider bcR = (b * c) as Element of F by A153;

                 A154:

                now

                  assume (MULTR . (a,bc)) = x;



                  then x = (aR * (bR * x)) by A151

                  .= ((aR * bR) * x) by GROUP_1:def 3

                  .= (x * x) by A144;

                  hence contradiction by A141;

                end;



                thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                .= ( multR (ab,c1)) by Def7

                .= ((aR * bR) * x) by A144, A145, A150, A141, Def6

                .= (aR * (bR * x)) by GROUP_1:def 3

                .= ( multR (a1,bc)) by A83, A152, A151, A154, Def6

                .= (( multR (x,o)) . (a,bc)) by Def7

                .= (a * (b * c)) by Def8;

              end;

                suppose

                 A156: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A157: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A157;

                per cases ;

                  suppose

                   A158: (MULTR . (b,c)) <> x;



                   A159: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (bR * cR) by A156, A139, A158, Def6;

                  then

                   A160: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A161: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b * c) as Element of C by Def8;

                  reconsider bcR = (b * c) as Element of F by A161;

                  per cases ;

                    suppose

                     A162: (MULTR . (x,c)) <> x;

                     A163:

                    now

                      assume (MULTR . (a,bc)) = x;



                      then x = (aR * (bR * cR)) by A159

                      .= ((aR * bR) * cR) by GROUP_1:def 3

                      .= (x * cR) by A144;

                      hence contradiction by A162;

                    end;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * bR) * cR) by A144, A145, A156, A162, Def6

                    .= (aR * (bR * cR)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A83, A163, A159, A160, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A164: (MULTR . (x,c)) = x;



                     A165: (aR * (bR * cR)) = ((aR * bR) * cR) by GROUP_1:def 3

                    .= x by A144, A164;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A164, A145, A156, Def6

                    .= ( multR (a1,bc)) by A165, A83, A160, A159, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

                  suppose

                   A166: (MULTR . (b,c)) = x;



                  then (bR * cR) = (aR * bR) by A144

                  .= (bR * aR) by GROUP_1:def 12;

                  then

                   A167: cR = aR by A146, ALGSTR_0:def 36, ALGSTR_0:def 20;



                   A168: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A156, A139, A166, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                   A169: (x * cR) = (aR * x) by A167, GROUP_1:def 12

                  .= (MULTR . (a,x));

                  per cases ;

                    suppose

                     A170: (MULTR . (x,c)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= (x * cR) by A145, A156, A170, Def6

                    .= ( multR (a1,bc)) by A83, A169, A170, A168, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A171: (MULTR . (x,c)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A145, A156, A171, Def6

                    .= ( multR (a1,bc)) by A83, A169, A171, A168, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

              end;

            end;

              suppose

               A172: (MULTR . (a,b)) <> x;



               A173: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (aR * bR) by A172, A139, A83, Def6;

              then

               A174: (a * b) <> o by A1;

              then not (a * b) in {o} by TARSKI:def 1;

              then

               A175: (a * b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider ab = (a * b) as Element of C by Def8;

              reconsider abR = (a * b) as Element of F by A175;

              per cases ;

                suppose

                 A176: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A177: (MULTR . (b,x)) <> x;



                   A178: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (bR * x) by A176, A139, A177, Def6;

                  then

                   A179: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A180: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b * c) as Element of C by Def8;

                  reconsider bcR = (b * c) as Element of F by A180;



                   A181: (MULTR . (ab,x)) = ((aR * bR) * x) by A173

                  .= (aR * (bR * x)) by GROUP_1:def 3

                  .= (MULTR . (a,bc)) by A178;

                  per cases ;

                    suppose

                     A182: (MULTR . (ab,x)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * bR) * x) by A173, A1, A176, A182, Def6

                    .= (aR * (bR * x)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A83, A182, A181, A178, A179, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A183: (MULTR . (ab,x)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A174, A176, A183, Def6

                    .= ( multR (a1,bc)) by A83, A183, A181, A179, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

                  suppose

                   A184: (MULTR . (b,x)) = x;



                   A185: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A176, A139, A184, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                   A186: ((aR * bR) * x) = (aR * (bR * x)) by GROUP_1:def 3

                  .= (MULTR . (a,x)) by A184;

                  per cases ;

                    suppose

                     A187: (MULTR . (ab,x)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * bR) * x) by A173, A1, A176, A187, Def6

                    .= ( multR (a1,bc)) by A173, A83, A187, A185, A186, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A188: (MULTR . (ab,x)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A174, A176, A188, Def6

                    .= ( multR (a1,bc)) by A173, A83, A188, A185, A186, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

              end;

                suppose

                 A189: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A190: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A190;

                per cases ;

                  suppose

                   A191: (MULTR . (b,c)) <> x;



                   A192: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= (bR * cR) by A189, A139, A191, Def6;

                  then

                   A193: (b * c) <> o by A1;

                  then not (b * c) in {o} by TARSKI:def 1;

                  then

                   A194: (b * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc = (b * c) as Element of C by Def8;

                  reconsider bcR = (b * c) as Element of F by A194;



                   A195: (MULTR . (ab,c)) = ((aR * bR) * cR) by A173

                  .= (aR * (bR * cR)) by GROUP_1:def 3

                  .= (MULTR . (a,bc)) by A192;

                  per cases ;

                    suppose

                     A196: (MULTR . (ab,c)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * bR) * cR) by A173, A174, A189, A196, Def6

                    .= (aR * (bR * cR)) by GROUP_1:def 3

                    .= ( multR (a1,bc)) by A193, A83, A196, A192, A195, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A197: (MULTR . (ab,c)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A174, A189, A197, Def6

                    .= ( multR (a1,bc)) by A193, A83, A197, A195, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

                  suppose

                   A198: (MULTR . (b,c)) = x;



                   A199: (b * c) = (( multR (x,o)) . (b1,c1)) by Def8

                  .= ( multR (b1,c1)) by Def7

                  .= o by A189, A139, A198, Def6;

                  then (b * c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc = (b * c) as Element of C by XBOOLE_0:def 3;



                   A200: ((aR * bR) * cR) = (aR * (bR * cR)) by GROUP_1:def 3

                  .= (MULTR . (a,x)) by A198;

                  per cases ;

                    suppose

                     A201: (MULTR . (ab,c)) <> x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= ((aR * bR) * cR) by A173, A174, A189, A201, Def6

                    .= ( multR (a1,bc)) by A173, A83, A201, A199, A200, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                    suppose

                     A202: (MULTR . (ab,c)) = x;



                    thus ((a * b) * c) = (( multR (x,o)) . (ab,c1)) by Def8

                    .= ( multR (ab,c1)) by Def7

                    .= o by A174, A189, A202, Def6

                    .= ( multR (a1,bc)) by A173, A83, A202, A199, A200, Def6

                    .= (( multR (x,o)) . (a,bc)) by Def7

                    .= (a * (b * c)) by Def8;

                  end;

                end;

              end;

            end;

          end;

        end;

      end;

      hence ( ExField (x,o)) is associative;

    end;

    theorem :: FIELD_3:11



     Th11: for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( ExField (x,o)) is distributive

    proof

      let x be non trivial Element of F;

      let o be object;

      assume not o in ( [#] F);

      then

       A1: a <> o;

      set C = ( carr (x,o)), E = ( ExField (x,o));



       A2: ( [#] E) = C by Def8;

       A3:

      now

        assume (x + x) = x;

        then x = ( 0. F) by RLVECT_1: 9;

        hence contradiction by Def2;

      end;

      then not (x + x) in {x} by TARSKI:def 1;

      then (x + x) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

      then

      reconsider xpx = (x + x) as Element of C by XBOOLE_0:def 3;



       A4: x <> ( 0. F) by Def2;

      then

       A5: x is left_mult-cancelable by ALGSTR_0:def 36;

       A6:

      now

        assume (x * x) = x;

        then (x * x) = (x * ( 1. F));

        hence contradiction by A5, ALGSTR_0:def 20, Def2;

      end;

      then not (x * x) in {x} by TARSKI:def 1;

      then (x * x) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

      then

      reconsider xmx = (x * x) as Element of C by XBOOLE_0:def 3;



       A7: (x * x) <> o by A1;

       A8:

      now

        assume ((x * x) + x) = x;

        then (x * x) = ( 0. F) by RLVECT_1: 9;

        then x = ( 0. F) by VECTSP_2:def 1;

        hence contradiction by Def2;

      end;

      then not ((x * x) + x) in {x} by TARSKI:def 1;

      then ((x * x) + x) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

      then

      reconsider xmxpx = ((x * x) + x) as Element of C by XBOOLE_0:def 3;

       A9:

      now

        let a,b,c be Element of E;

        per cases ;

          suppose

           A10: a = o;

          then a in {o} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of C by XBOOLE_0:def 3;

          per cases ;

            suppose

             A11: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of C by XBOOLE_0:def 3;



             A12: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

            .= ( multR (a1,b1)) by Def7

            .= (x * x) by A10, A11, A6, Def6;

            per cases ;

              suppose

               A13: c = o;

              then c in {o} by TARSKI:def 1;

              then

              reconsider c1 = c as Element of C by XBOOLE_0:def 3;



               A14: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

              .= ( addR (b1,c1)) by Def5

              .= (x + x) by A13, A11, A3, Def4;



               A15: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

              .= ( multR (a1,c1)) by Def7

              .= (x * x) by A13, A10, A6, Def6;



               A16: ((x * x) + (x * x)) = (x * (x + x)) by VECTSP_1:def 2;

              per cases ;

                suppose

                 A17: ((x * x) + (x * x)) <> x;



                 A18: xpx <> o & xmx <> o by A1;



                thus ((a * b) + (a * c)) = (( addR (x,o)) . (xmx,xmx)) by A15, A12, Def8

                .= ( addR (xmx,xmx)) by Def5

                .= ((x * x) + (x * x)) by A18, A17, Def4

                .= ( multR (a1,xpx)) by A1, A17, A10, A16, Def6

                .= (( multR (x,o)) . (a1,xpx)) by Def7

                .= (a * (b + c)) by A14, Def8;

              end;

                suppose

                 A19: ((x * x) + (x * x)) = x;



                 A20: xpx <> o & xmx <> o by A1;



                thus ((a * b) + (a * c)) = (( addR (x,o)) . (xmx,xmx)) by A15, A12, Def8

                .= ( addR (xmx,xmx)) by Def5

                .= o by A20, A19, Def4

                .= ( multR (a1,xpx)) by A20, A19, A10, A16, Def6

                .= (( multR (x,o)) . (a1,xpx)) by Def7

                .= (a * (b + c)) by A14, Def8;

              end;

            end;

              suppose

               A21: c <> o;

              then not c in {o} by TARSKI:def 1;

              then

               A22: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider c1 = c as Element of C by Def8;

              reconsider cR = c as Element of F by A22;

              per cases ;

                suppose

                 A23: (x + cR) = x;

                then

                 A24: cR = ( 0. F) by RLVECT_1: 9;



                 A25: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= o by A23, A21, A11, Def4;

                then (b + c) in {o} by TARSKI:def 1;

                then

                reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;



                 A26: (x * cR) <> x by A24, Def2;



                 A27: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= (x * cR) by A26, A21, A10, Def6;

                then

                 A28: (a * c) <> o by A1;

                reconsider ac1 = (a * c) as Element of C by Def8;

                 A29:

                now

                  assume ((x * x) + (x * cR)) = x;

                  then (x * (x + cR)) = (x * ( 1. F)) by VECTSP_1:def 2;

                  then (x + cR) = ( 1. F) by A4, VECTSP_2: 8;

                  hence contradiction by A23, Def2;

                end;



                thus ((a * b) + (a * c)) = (( addR (x,o)) . (xmx,ac1)) by A12, Def8

                .= ( addR (xmx,ac1)) by Def5

                .= ((x * x) + (x * cR)) by A7, A28, A27, A29, Def4

                .= (x * x) by A23, VECTSP_1:def 2

                .= ( multR (a1,bc1)) by A10, A25, A6, Def6

                .= (( multR (x,o)) . (a1,bc1)) by Def7

                .= (a * (b + c)) by Def8;

              end;

                suppose

                 A30: (x + cR) <> x;



                 A31: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (x + cR) by A30, A21, A11, Def4;

                then

                 A32: (b + c) <> o by A1;

                then not (b + c) in {o} by TARSKI:def 1;

                then

                 A33: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider bc1 = (b + c) as Element of C by Def8;

                reconsider bcR = (b + c) as Element of F by A33;

                per cases ;

                  suppose

                   A34: (x * cR) = x;



                   A35: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                  .= ( multR (a1,c1)) by Def7

                  .= o by A34, A21, A10, Def6;

                  then (a * c) in {o} by TARSKI:def 1;

                  then

                  reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                   A36: (x * (x + cR)) <> x by A34, A8, VECTSP_1:def 2;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (xmx,ac1)) by A12, Def8

                  .= ( addR (xmx,ac1)) by Def5

                  .= ((x * x) + x) by A8, A1, A35, Def4

                  .= (x * (x + cR)) by A34, VECTSP_1:def 2

                  .= ( multR (a1,bc1)) by A10, A31, A1, A36, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

                  suppose

                   A37: (x * cR) <> x;



                   A38: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                  .= ( multR (a1,c1)) by Def7

                  .= (x * cR) by A37, A21, A10, Def6;

                  then

                   A39: (a * c) <> o by A1;

                  then not (a * c) in {o} by TARSKI:def 1;

                  then

                   A40: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider ac1 = (a * c) as Element of C by Def8;

                  reconsider acR = (a * c) as Element of F by A40;

                  per cases ;

                    suppose

                     A41: ((x * x) + (x * cR)) <> x;

                    then

                     A42: (x * (x + cR)) <> x by VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (xmx,ac1)) by A12, Def8

                    .= ( addR (xmx,ac1)) by Def5

                    .= ((x * x) + (x * cR)) by A41, A7, A38, A39, Def4

                    .= (x * (x + cR)) by VECTSP_1:def 2

                    .= ( multR (a1,bc1)) by A42, A10, A31, A1, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A43: ((x * x) + (x * cR)) = x;

                    then

                     A44: (x * (x + cR)) = x by VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (xmx,ac1)) by A12, Def8

                    .= ( addR (xmx,ac1)) by Def5

                    .= o by A43, A7, A38, A39, Def4

                    .= ( multR (a1,bc1)) by A44, A10, A31, A32, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                end;

              end;

            end;

          end;

            suppose

             A45: b <> o;

            then not b in {o} by TARSKI:def 1;

            then

             A46: b in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

            reconsider b1 = b as Element of C by Def8;

            reconsider bR = b as Element of F by A46;

            per cases ;

              suppose

               A47: (x * bR) = x;



               A48: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A10, A45, A47, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab1 = (a * b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose

                 A49: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A50: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= (x * x) by A10, A49, A6, Def6;

                 A51:

                now

                  assume (bR + x) = x;

                  then bR = ( 0. F) by RLVECT_1: 9;

                  hence contradiction by A47, Def2;

                end;



                 A52: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (bR + x) by A51, A49, A45, Def4;

                then (b + c) <> o by A1;

                then not (b + c) in {o} by TARSKI:def 1;

                then

                 A53: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider bc1 = (b + c) as Element of C by Def8;



                 A54: (x * (bR + x)) = (x + (x * x)) by A47, VECTSP_1:def 2;

                reconsider bcR = (b + c) as Element of F by A53;



                thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,xmx)) by A50, Def8

                .= ( addR (ab1,xmx)) by Def5

                .= (x + (x * x)) by A8, A48, A1, Def4

                .= ( multR (a1,bc1)) by A10, A52, A8, A54, A1, Def6

                .= (( multR (x,o)) . (a1,bc1)) by Def7

                .= (a * (b + c)) by Def8;

              end;

                suppose

                 A55: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A56: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A56;

                per cases ;

                  suppose

                   A57: (bR + cR) = x;



                   A58: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A45, A55, A57, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A59: (x * cR) = x;



                     A60: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A10, A55, A59, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                     A61: (x * x) = (x + x)

                    proof



                       A62: x <> ( 0. F) by Def2;

                      (x * bR) = (x * ( 1. F)) by A47;

                      then

                       A63: bR = ( 1. F) by A62, VECTSP_2: 8;



                       A64: (x * cR) = (x * ( 1. F)) by A59;



                       A65: x = (( 1. F) + ( 1. F)) by A57, A62, A63, A64, VECTSP_2: 8;



                      hence (x * x) = ((( 1. F) * (( 1. F) + ( 1. F))) + (( 1. F) * (( 1. F) + ( 1. F)))) by VECTSP_1:def 3

                      .= (x + x) by A65;

                    end;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= (x + x) by A60, A48, A3, Def4

                    .= ( multR (a1,bc1)) by A61, A10, A58, A6, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A66: (x * cR) <> x;



                     A67: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (x * cR) by A10, A55, A66, Def6;

                    then (a * c) <> o by A1;

                    then not (a * c) in {o} by TARSKI:def 1;

                    then

                     A68: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    reconsider acR = (a * c) as Element of F by A68;



                     A69: (x * x) = (x + (x * cR)) by A47, A57, VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= (x + (x * cR)) by A1, A67, A48, A69, A6, Def4

                    .= ( multR (a1,bc1)) by A69, A10, A58, A6, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A70: (bR + cR) <> x;



                   A71: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A45, A55, A70, Def4;

                  then

                   A72: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A73: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A73;

                  per cases ;

                    suppose

                     A74: (x * cR) = x;



                     A75: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A10, A55, A74, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;

                     A76:

                    now

                      assume

                       A77: (x * (bR + cR)) = x;



                       A78: x <> ( 0. F) by Def2;

                      (x * ( 1. F)) = ((x * ( 1. F)) + (x * cR)) by A47, A77, VECTSP_1:def 2

                      .= (x * (( 1. F) + cR)) by VECTSP_1:def 2;

                      then ( 1. F) = (( 1. F) + cR) by A78, VECTSP_2: 8;

                      then cR = ( 0. F) by RLVECT_1: 9;

                      hence contradiction by A74, Def2;

                    end;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= (x + x) by A3, A75, A48, Def4

                    .= (x * (bR + cR)) by A74, A47, VECTSP_1:def 2

                    .= ( multR (a1,bc1)) by A76, A10, A1, A71, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A79: (x * cR) <> x;



                     A80: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (x * cR) by A10, A55, A79, Def6;

                    then

                     A81: (a * c) <> o by A1;

                    then not (a * c) in {o} by TARSKI:def 1;

                    then

                     A82: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    reconsider acR = (a * c) as Element of F by A82;



                     A83: (x * (bR + cR)) = (x + (x * cR)) by A47, VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A84: (x + (x * cR)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A81, A80, A48, A84, Def4

                      .= ( multR (a1,bc1)) by A84, A83, A10, A71, A72, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A85: (x + (x * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= (x + (x * cR)) by A1, A80, A48, A85, Def4

                      .= ( multR (a1,bc1)) by A85, A83, A10, A71, A1, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A86: (x * bR) <> x;



               A87: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (x * bR) by A10, A45, A86, Def6;

              then

               A88: (a * b) <> o by A1;

              then not (a * b) in {o} by TARSKI:def 1;

              then

               A89: (a * b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider ab1 = (a * b) as Element of C by Def8;

              reconsider abR = (a * b) as Element of F by A89;

              per cases ;

                suppose

                 A90: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A91: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= (x * x) by A10, A90, A6, Def6;

                then

                 A92: (a * c) <> o by A1;

                then not (a * c) in {o} by TARSKI:def 1;

                then

                 A93: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider ac1 = (a * c) as Element of C by Def8;

                reconsider acR = (a * c) as Element of F by A93;

                per cases ;

                  suppose

                   A94: (bR + x) = x;



                   A95: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A45, A90, A94, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;



                   A96: ((x * bR) + (x * x)) = (x * x) by A94, VECTSP_1:def 2;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= ((x * bR) + (x * x)) by A87, A88, A91, A92, A96, A6, Def4

                  .= ( multR (a1,bc1)) by A10, A95, A96, A6, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

                  suppose

                   A97: (bR + x) <> x;



                   A98: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + x) by A45, A90, A97, Def4;

                  then

                   A99: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A100: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A100;

                  per cases ;

                    suppose

                     A101: ((x * bR) + (x * x)) <> x;



                     A102: ((x * bR) + (x * x)) = (x * (bR + x)) by VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= ((x * bR) + (x * x)) by A87, A88, A91, A92, A101, Def4

                    .= ( multR (a1,bc1)) by A10, A98, A1, A101, A102, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A103: ((x * bR) + (x * x)) = x;



                     A104: ((x * bR) + (x * x)) = (x * (bR + x)) by VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= o by A87, A88, A91, A92, A103, Def4

                    .= ( multR (a1,bc1)) by A10, A98, A99, A103, A104, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                end;

              end;

                suppose

                 A105: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A106: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A106;

                per cases ;

                  suppose

                   A107: (bR + cR) = x;



                   A108: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A45, A105, A107, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;



                   A109: ((x * bR) + (x * cR)) = (x * x) by A107, VECTSP_1:def 2;

                  per cases ;

                    suppose

                     A110: (x * cR) <> x;



                     A111: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (x * cR) by A10, A105, A110, Def6;

                    then

                     A112: (a * c) <> o by A1;

                    then not (a * c) in {o} by TARSKI:def 1;

                    then

                     A113: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    reconsider acR = (a * c) as Element of F by A113;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= ((x * bR) + (x * cR)) by A87, A88, A111, A112, A109, A6, Def4

                    .= ( multR (a1,bc1)) by A10, A108, A6, A109, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A114: (x * cR) = x;



                     A115: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A10, A105, A114, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;

                     A116:

                    now

                      assume ((x * bR) + x) = x;

                      then

                       A117: (x * ( 1. F)) = (x * (bR + cR)) by A114, VECTSP_1:def 2;

                      x <> ( 0. F) by Def2;

                      then (bR + cR) = ( 1. F) by A117, VECTSP_2: 8;

                      hence contradiction by A107, Def2;

                    end;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= ((x * bR) + x) by A87, A1, A115, A116, Def4

                    .= ( multR (a1,bc1)) by A10, A108, A6, A109, A114, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                end;

                  suppose

                   A118: (bR + cR) <> x;



                   A119: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A45, A105, A118, Def4;

                  then

                   A120: (b + c) <> o by A1;

                  then not (b + c) in {o} by TARSKI:def 1;

                  then

                   A121: (b + c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                  reconsider bcR = (b + c) as Element of F by A121;



                   A122: ((x * bR) + (x * cR)) = (x * (bR + cR)) by VECTSP_1:def 2;

                  per cases ;

                    suppose

                     A123: (x * cR) <> x;



                     A124: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (x * cR) by A10, A105, A123, Def6;

                    then

                     A125: (a * c) <> o by A1;

                    then not (a * c) in {o} by TARSKI:def 1;

                    then

                     A126: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    reconsider acR = (a * c) as Element of F by A126;

                    per cases ;

                      suppose

                       A127: ((x * bR) + (x * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((x * bR) + (x * cR)) by A87, A88, A124, A125, A127, Def4

                      .= ( multR (a1,bc1)) by A10, A119, A1, A127, A122, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A128: ((x * bR) + (x * cR)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A87, A88, A124, A125, A128, Def4

                      .= ( multR (a1,bc1)) by A10, A119, A120, A128, A122, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                    suppose

                     A129: (x * cR) = x;



                     A130: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A10, A105, A129, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                     A131: ((x * bR) + x) = (x * (bR + cR)) by A129, VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A132: ((x * bR) + x) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((x * bR) + x) by A87, A1, A130, A132, Def4

                      .= ( multR (a1,bc1)) by A10, A119, A1, A132, A131, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A133: ((x * bR) + x) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A87, A88, A130, A133, Def4

                      .= ( multR (a1,bc1)) by A10, A119, A120, A133, A131, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

              end;

            end;

          end;

        end;

          suppose

           A134: a <> o;

          then not a in {o} by TARSKI:def 1;

          then

           A135: a in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

          reconsider a1 = a as Element of ( carr (x,o)) by Def8;

          reconsider aR = a as Element of ( [#] F) by A135;

          per cases ;

            suppose

             A136: b = o;

            then b in {o} by TARSKI:def 1;

            then

            reconsider b1 = b as Element of C by XBOOLE_0:def 3;

            per cases ;

              suppose

               A137: (aR * x) = x;



               A138: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A134, A136, A137, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab1 = (a * b) as Element of C by XBOOLE_0:def 3;

              per cases ;

                suppose

                 A139: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A140: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= o by A134, A139, A137, Def6;

                then (a * c) in {o} by TARSKI:def 1;

                then

                reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                 A141: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (x + x) by A136, A139, A3, Def4;

                then

                 A142: (b + c) <> o by A1;

                reconsider bc1 = (b + c) as Element of C by Def8;



                 A143: (aR * (x + x)) = (x + x) by A137, VECTSP_1:def 2;



                thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                .= ( addR (ab1,ac1)) by Def5

                .= (x + x) by A140, A138, A3, Def4

                .= ( multR (a1,bc1)) by A143, A142, A134, A141, A3, Def6

                .= (( multR (x,o)) . (a1,bc1)) by Def7

                .= (a * (b + c)) by Def8;

              end;

                suppose

                 A144: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A145: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of ( carr (x,o)) by Def8;

                reconsider cR = c as Element of ( [#] F) by A145;

                 A146:

                now

                  assume

                   A147: (aR * cR) = x;

                  aR <> ( 0. F) by A137, Def2;

                  then cR = x by A137, A147, VECTSP_2: 8;

                  then cR in {x} by TARSKI:def 1;

                  hence contradiction by A145, XBOOLE_0:def 5;

                end;



                 A148: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= (aR * cR) by A134, A144, A146, Def6;

                then

                 A149: (a * c) <> o by A1;

                reconsider ac1 = (a * c) as Element of C by Def8;

                per cases ;

                  suppose

                   A150: (x + cR) = x;

                  then

                   A151: ((aR * x) + (aR * cR)) = (aR * x) by VECTSP_1:def 2;



                   A152: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A144, A136, A150, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= o by A137, A138, A148, A149, A151, Def4

                  .= ( multR (a1,bc1)) by A134, A152, A137, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

                  suppose

                   A153: (x + cR) <> x;



                   A154: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (x + cR) by A136, A144, A153, Def4;

                  then

                   A155: (b + c) <> o by A1;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                   A156:

                  now

                    assume (x + (aR * cR)) = x;

                    then

                     A158: (aR * x) = (aR * (x + cR)) by A137, VECTSP_1:def 2;

                    aR <> ( 0. F) by A137, Def2;

                    hence contradiction by A153, A158, VECTSP_2: 8;

                  end;



                   A159: (x + (aR * cR)) = (aR * (x + cR)) by A137, VECTSP_1:def 2;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= (x + (aR * cR)) by A138, A148, A1, A156, Def4

                  .= ( multR (a1,bc1)) by A134, A154, A155, A156, A159, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

              end;

            end;

              suppose

               A160: (aR * x) <> x;



               A161: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (aR * x) by A134, A136, A160, Def6;

              then

               A162: (a * b) <> o by A1;

              then not (a * b) in {o} by TARSKI:def 1;

              then

               A163: (a * b) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

              reconsider ab1 = (a * b) as Element of C by Def8;

              reconsider abR = (a * b) as Element of F by A163;

              per cases ;

                suppose

                 A164: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A165: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= (aR * x) by A134, A164, A160, Def6;

                then

                 A166: (a * c) <> o by A1;

                reconsider ac1 = (a * c) as Element of C by Def8;



                 A167: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (x + x) by A136, A164, A3, Def4;

                then

                 A168: (b + c) <> o by A1;

                reconsider bc1 = (b + c) as Element of C by Def8;



                 A169: (aR * (x + x)) = ((aR * x) + (aR * x)) by VECTSP_1:def 2;

                per cases ;

                  suppose

                   A170: ((aR * x) + (aR * x)) <> x;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= ((aR * x) + (aR * x)) by A161, A165, A166, A170, Def4

                  .= ( multR (a1,bc1)) by A134, A170, A169, A168, A167, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

                  suppose

                   A171: ((aR * x) + (aR * x)) = x;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= o by A161, A165, A166, A171, Def4

                  .= ( multR (a1,bc1)) by A134, A171, A169, A168, A167, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

              end;

                suppose

                 A172: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A173: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of ( carr (x,o)) by Def8;

                reconsider cR = c as Element of ( [#] F) by A173;

                per cases ;

                  suppose

                   A174: (aR * cR) = x;



                   A175: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                  .= ( multR (a1,c1)) by Def7

                  .= o by A134, A172, A174, Def6;

                  then (a * c) in {o} by TARSKI:def 1;

                  then

                  reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A176: (x + cR) = x;



                     A177: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                    .= ( addR (b1,c1)) by Def5

                    .= o by A136, A172, A176, Def4;

                    then (b + c) in {o} by TARSKI:def 1;

                    then

                    reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;



                     A178: ((aR * x) + x) = (aR * x) by A176, A174, VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= ((aR * x) + x) by A160, A161, A1, A175, A178, Def4

                    .= ( multR (a1,bc1)) by A134, A177, A178, A160, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A179: (x + cR) <> x;



                     A180: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                    .= ( addR (b1,c1)) by Def5

                    .= (x + cR) by A136, A172, A179, Def4;

                    then

                     A181: (b + c) <> o by A1;

                    reconsider bc1 = (b + c) as Element of C by Def8;



                     A182: ((aR * x) + x) = (aR * (x + cR)) by A174, VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A183: ((aR * x) + x) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * x) + x) by A161, A1, A175, A183, Def4

                      .= ( multR (a1,bc1)) by A134, A180, A181, A183, A182, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A184: ((aR * x) + x) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A161, A162, A175, A184, Def4

                      .= ( multR (a1,bc1)) by A134, A180, A181, A184, A182, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

                  suppose

                   A185: (aR * cR) <> x;



                   A186: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                  .= ( multR (a1,c1)) by Def7

                  .= (aR * cR) by A134, A172, A185, Def6;

                  then

                   A187: (a * c) <> o by A1;

                  reconsider ac1 = (a * c) as Element of C by Def8;

                  per cases ;

                    suppose

                     A188: (x + cR) = x;



                     A189: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                    .= ( addR (b1,c1)) by Def5

                    .= o by A136, A172, A188, Def4;

                    then (b + c) in {o} by TARSKI:def 1;

                    then

                    reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;



                     A190: ((aR * x) + (aR * cR)) = (aR * x) by A188, VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= ((aR * x) + (aR * cR)) by A160, A161, A162, A186, A187, A190, Def4

                    .= ( multR (a1,bc1)) by A160, A134, A189, A190, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A191: (x + cR) <> x;



                     A192: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                    .= ( addR (b1,c1)) by Def5

                    .= (x + cR) by A136, A172, A191, Def4;

                    then

                     A193: (b + c) <> o by A1;

                    reconsider bc1 = (b + c) as Element of C by Def8;



                     A194: ((aR * x) + (aR * cR)) = (aR * (x + cR)) by VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A195: ((aR * x) + (aR * cR)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A161, A162, A186, A187, A195, Def4

                      .= ( multR (a1,bc1)) by A134, A192, A193, A195, A194, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A196: ((aR * x) + (aR * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * x) + (aR * cR)) by A161, A162, A186, A187, A196, Def4

                      .= ( multR (a1,bc1)) by A134, A192, A193, A196, A194, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

              end;

            end;

          end;

            suppose

             A197: b <> o;

            then not b in {o} by TARSKI:def 1;

            then

             A198: b in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

            reconsider b1 = b as Element of ( carr (x,o)) by Def8;

            reconsider bR = b as Element of ( [#] F) by A198;

            per cases ;

              suppose

               A199: (aR * bR) = x;



               A200: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= o by A134, A197, A199, Def6;

              then (a * b) in {o} by TARSKI:def 1;

              then

              reconsider ab1 = (a * b) as Element of C by XBOOLE_0:def 3;



               A201: (aR * (bR + x)) = (x + (aR * x)) by A199, VECTSP_1:def 2;

               A202:

              now

                assume (bR + x) = x;

                then bR = ( 0. F) by RLVECT_1: 9;

                hence contradiction by A199, Def2;

              end;

               A203:

              now

                assume (aR * x) = x;

                then

                 A205: (x * aR) = (x * ( 1. F)) by GROUP_1:def 12;

                x <> ( 0. F) by Def2;

                then aR = ( 1. F) by A205, VECTSP_2: 8;

                then bR in {x} by A199, TARSKI:def 1;

                hence contradiction by A198, XBOOLE_0:def 5;

              end;

              per cases ;

                suppose

                 A206: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;



                 A207: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                .= ( addR (b1,c1)) by Def5

                .= (bR + x) by A197, A206, A202, Def4;

                then

                 A208: (b + c) <> o by A1;

                reconsider bc1 = (b + c) as Element of C by Def8;

                reconsider bcR = (b + c) as Element of F by A207;



                 A209: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                .= ( multR (a1,c1)) by Def7

                .= (aR * x) by A134, A206, A203, Def6;

                then

                 A210: (a * c) <> o by A1;

                then not (a * c) in {o} by TARSKI:def 1;

                then

                 A211: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider ac1 = (a * c) as Element of C by Def8;

                reconsider acR = (a * c) as Element of F by A211;

                per cases ;

                  suppose

                   A212: (x + (aR * x)) = x;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= o by A200, A209, A210, A212, Def4

                  .= ( multR (a1,bc1)) by A201, A134, A207, A208, A212, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

                  suppose

                   A213: (x + (aR * x)) <> x;



                  thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                  .= ( addR (ab1,ac1)) by Def5

                  .= (x + (aR * x)) by A200, A209, A1, A213, Def4

                  .= ( multR (a1,bc1)) by A201, A134, A207, A208, A213, Def6

                  .= (( multR (x,o)) . (a1,bc1)) by Def7

                  .= (a * (b + c)) by Def8;

                end;

              end;

                suppose

                 A214: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A215: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A215;

                per cases ;

                  suppose

                   A216: (bR + cR) = x;



                   A217: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A197, A214, A216, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A218: (aR * cR) = x;



                     A219: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A134, A214, A218, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= (x + x) by A200, A219, A3, Def4

                    .= (aR * x) by A216, A218, A199, VECTSP_1:def 2

                    .= ( multR (a1,bc1)) by A134, A217, A203, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A220: (aR * cR) <> x;



                     A221: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (aR * cR) by A134, A214, A220, Def6;

                    then not (a * c) = o by A1;

                    then not (a * c) in {o} by TARSKI:def 1;

                    then

                     A222: (a * c) in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    reconsider acR = (a * c) as Element of F by A222;



                     A223: (x + (aR * cR)) = (aR * x) by A216, A199, VECTSP_1:def 2;

                    per cases ;

                      suppose (x + (aR * cR)) = x;

                      hence ((a * b) + (a * c)) = (a * (b + c)) by A203, A216, A199, VECTSP_1:def 2;

                    end;

                      suppose

                       A225: (x + (aR * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= (x + (aR * cR)) by A200, A221, A1, A225, Def4

                      .= ( multR (a1,bc1)) by A134, A217, A225, A223, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

                  suppose

                   A226: (bR + cR) <> x;



                   A227: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A197, A214, A226, Def4;

                  then

                   A228: (b + c) <> o by A1;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                  per cases ;

                    suppose

                     A229: (aR * cR) = x;



                     A230: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A134, A214, A229, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                     A231: (aR * (bR + cR)) = (x + x) by A229, A199, VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= (x + x) by A200, A230, A3, Def4

                    .= ( multR (a1,bc1)) by A3, A231, A134, A228, A227, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A232: (aR * cR) <> x;



                     A233: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (aR * cR) by A134, A214, A232, Def6;

                    then

                     A234: not (a * c) = o by A1;

                    reconsider ac1 = (a * c) as Element of C by Def8;



                     A235: (x + (aR * cR)) = (aR * (bR + cR)) by A199, VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A236: (x + (aR * cR)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A200, A233, A234, A236, Def4

                      .= ( multR (a1,bc1)) by A134, A227, A228, A236, A235, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A237: (x + (aR * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= (x + (aR * cR)) by A200, A233, A1, A237, Def4

                      .= ( multR (a1,bc1)) by A134, A227, A228, A237, A235, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A238: (aR * bR) <> x;



               A239: (a * b) = (( multR (x,o)) . (a1,b1)) by Def8

              .= ( multR (a1,b1)) by Def7

              .= (aR * bR) by A134, A197, A238, Def6;

              then

               A240: (a * b) <> o by A1;

              reconsider ab1 = (a * b) as Element of C by Def8;

              reconsider abR = (a * b) as Element of F by A239;

              per cases ;

                suppose

                 A241: c = o;

                then c in {o} by TARSKI:def 1;

                then

                reconsider c1 = c as Element of C by XBOOLE_0:def 3;

                per cases ;

                  suppose

                   A242: (bR + x) <> x;



                   A243: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + x) by A197, A241, A242, Def4;

                  then

                   A244: (b + c) <> o by A1;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                  per cases ;

                    suppose

                     A245: (aR * x) <> x;



                     A246: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (aR * x) by A134, A241, A245, Def6;

                    then

                     A247: (a * c) <> o by A1;

                    reconsider ac1 = (a * c) as Element of C by Def8;



                     A248: ((aR * bR) + (aR * x)) = (aR * (bR + x)) by VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A249: ((aR * bR) + (aR * x)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * bR) + (aR * x)) by A240, A239, A246, A247, A249, Def4

                      .= ( multR (a1,bc1)) by A134, A243, A244, A249, A248, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A250: ((aR * bR) + (aR * x)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A240, A239, A246, A247, A250, Def4

                      .= ( multR (a1,bc1)) by A134, A243, A244, A250, A248, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                    suppose

                     A251: (aR * x) = x;



                     A252: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A134, A241, A251, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                     A253: ((aR * bR) + x) = (aR * (bR + x)) by A251, VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A254: ((aR * bR) + x) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * bR) + x) by A1, A239, A252, A254, Def4

                      .= ( multR (a1,bc1)) by A134, A243, A244, A254, A253, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A255: ((aR * bR) + x) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A240, A239, A252, A255, Def4

                      .= ( multR (a1,bc1)) by A134, A243, A244, A255, A253, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

                  suppose

                   A256: (bR + x) = x;



                   A257: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A197, A241, A256, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A258: (aR * x) <> x;



                     A259: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (aR * x) by A134, A241, A258, Def6;

                    then

                     A260: (a * c) <> o by A1;

                    reconsider ac1 = (a * c) as Element of C by Def8;



                     A261: ((aR * bR) + (aR * x)) = (aR * x) by A256, VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= (aR * x) by A240, A239, A259, A260, A258, A261, Def4

                    .= ( multR (a1,bc1)) by A258, A134, A257, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                    suppose

                     A262: (aR * x) = x;



                     A263: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A134, A241, A262, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                     A264: ((aR * bR) + x) = x by A256, A262, VECTSP_1:def 2;



                    thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                    .= ( addR (ab1,ac1)) by Def5

                    .= o by A240, A239, A263, A264, Def4

                    .= ( multR (a1,bc1)) by A262, A134, A257, Def6

                    .= (( multR (x,o)) . (a1,bc1)) by Def7

                    .= (a * (b + c)) by Def8;

                  end;

                end;

              end;

                suppose

                 A265: c <> o;

                then not c in {o} by TARSKI:def 1;

                then

                 A266: c in (( [#] F) \ {x}) by A2, XBOOLE_0:def 3;

                reconsider c1 = c as Element of C by Def8;

                reconsider cR = c as Element of F by A266;



                 A267: ((aR * bR) + (aR * cR)) = (aR * (bR + cR)) by VECTSP_1:def 2;

                per cases ;

                  suppose

                   A268: (bR + cR) <> x;



                   A269: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= (bR + cR) by A197, A265, A268, Def4;

                  then

                   A270: (b + c) <> o by A1;

                  reconsider bc1 = (b + c) as Element of C by Def8;

                  per cases ;

                    suppose

                     A271: (aR * cR) <> x;



                     A272: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (aR * cR) by A134, A265, A271, Def6;

                    then

                     A273: (a * c) <> o by A1;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    per cases ;

                      suppose

                       A274: ((aR * bR) + (aR * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * bR) + (aR * cR)) by A240, A239, A272, A273, A274, Def4

                      .= ( multR (a1,bc1)) by A134, A269, A270, A274, A267, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A275: ((aR * bR) + (aR * cR)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A240, A239, A272, A273, A275, Def4

                      .= ( multR (a1,bc1)) by A134, A269, A270, A275, A267, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                    suppose

                     A276: (aR * cR) = x;



                     A277: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A134, A265, A276, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;

                    per cases ;

                      suppose

                       A278: ((aR * bR) + x) <> x;

                      then

                       A279: (aR * (bR + cR)) <> x by A276, VECTSP_1:def 2;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * bR) + x) by A1, A239, A277, A278, Def4

                      .= (aR * (bR + cR)) by A276, VECTSP_1:def 2

                      .= ( multR (a1,bc1)) by A134, A269, A270, A279, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A280: ((aR * bR) + x) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A240, A239, A277, A280, Def4

                      .= ( multR (a1,bc1)) by A267, A276, A134, A269, A270, A280, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

                  suppose

                   A281: (bR + cR) = x;



                   A282: (b + c) = (( addR (x,o)) . (b1,c1)) by Def8

                  .= ( addR (b1,c1)) by Def5

                  .= o by A197, A265, A281, Def4;

                  then (b + c) in {o} by TARSKI:def 1;

                  then

                  reconsider bc1 = (b + c) as Element of C by XBOOLE_0:def 3;

                  per cases ;

                    suppose

                     A283: (aR * cR) <> x;



                     A284: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= (aR * cR) by A134, A265, A283, Def6;

                    then

                     A285: (a * c) <> o by A1;

                    reconsider ac1 = (a * c) as Element of C by Def8;

                    per cases ;

                      suppose

                       A286: ((aR * bR) + (aR * cR)) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * bR) + (aR * cR)) by A240, A239, A284, A285, A286, Def4

                      .= ( multR (a1,bc1)) by A286, A134, A281, A282, A267, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A287: ((aR * bR) + (aR * cR)) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A240, A239, A284, A285, A287, Def4

                      .= ( multR (a1,bc1)) by A287, A134, A281, A282, A267, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                    suppose

                     A288: (aR * cR) = x;



                     A289: (a * c) = (( multR (x,o)) . (a1,c1)) by Def8

                    .= ( multR (a1,c1)) by Def7

                    .= o by A134, A265, A288, Def6;

                    then (a * c) in {o} by TARSKI:def 1;

                    then

                    reconsider ac1 = (a * c) as Element of C by XBOOLE_0:def 3;



                     A290: ((aR * bR) + x) = (aR * (bR + cR)) by A288, VECTSP_1:def 2;

                    per cases ;

                      suppose

                       A291: ((aR * bR) + x) <> x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= ((aR * bR) + x) by A1, A239, A289, A291, Def4

                      .= ( multR (a1,bc1)) by A291, A134, A281, A282, A290, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                      suppose

                       A292: ((aR * bR) + x) = x;



                      thus ((a * b) + (a * c)) = (( addR (x,o)) . (ab1,ac1)) by Def8

                      .= ( addR (ab1,ac1)) by Def5

                      .= o by A240, A239, A289, A292, Def4

                      .= ( multR (a1,bc1)) by A292, A134, A281, A282, A290, Def6

                      .= (( multR (x,o)) . (a1,bc1)) by Def7

                      .= (a * (b + c)) by Def8;

                    end;

                  end;

                end;

              end;

            end;

          end;

        end;

      end;

      now

        let a,b,c be Element of ( ExField (x,o));

        thus (a * (b + c)) = ((a * b) + (a * c)) by A9;



        thus ((b + c) * a) = (a * (b + c)) by GROUP_1:def 12

        .= ((a * b) + (a * c)) by A9

        .= ((b * a) + (a * c)) by GROUP_1:def 12

        .= ((b * a) + (c * a)) by GROUP_1:def 12;

      end;

      hence ( ExField (x,o)) is distributive;

    end;

    theorem :: FIELD_3:12



     Th12: for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( ExField (x,o)) is almost_left_invertible

    proof

      let x be non trivial Element of F;

      let v be object;

      assume not v in ( [#] F);

      then

       A1: a <> v;

      x <> ( 0. F) by Def2;

      then

      consider xi be Element of F such that

       A2: (xi * x) = ( 1. F) by ALGSTR_0:def 39, ALGSTR_0:def 27;



       A3: ( [#] ( ExField (x,v))) = ( carr (x,v)) by Def8;

      v in {v} by TARSKI:def 1;

      then

      reconsider u1 = v as Element of ( carr (x,v)) by XBOOLE_0:def 3;

      reconsider u = u1 as Element of ( ExField (x,v)) by Def8;

      now

        let a be Element of ( ExField (x,v));

        assume

         A4: a <> ( 0. ( ExField (x,v)));

        ( 0. F) <> x by Def2;

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

        then ( 0. F) in (( [#] F) \ {x}) by XBOOLE_0:def 5;

        then

        reconsider o = ( 0. F) as Element of ( carr (x,v)) by XBOOLE_0:def 3;

        per cases ;

          suppose

           A5: a = v;

          then a in {v} by TARSKI:def 1;

          then

          reconsider a1 = a as Element of ( carr (x,v)) by XBOOLE_0:def 3;

          per cases ;

            suppose

             A6: xi = x;

            then

             A7: (the multF of F . (x,x)) <> x by A2, Def2;

            (u * a) = (( multR (x,v)) . (u1,a1)) by Def8

            .= ( multR (u1,a1)) by Def7

            .= (the multF of F . (xi,x)) by A7, A6, A5, Def6

            .= ( 1. ( ExField (x,v))) by A2, Def8;

            hence a is left_invertible by ALGSTR_0:def 27;

          end;

            suppose xi <> x;

            then not xi in {x} by TARSKI:def 1;

            then xi in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider x1i = xi as Element of ( carr (x,v)) by XBOOLE_0:def 3;

            reconsider b = x1i as Element of ( ExField (x,v)) by Def8;



             A8: (the multF of F . (b,x)) <> x by A2, Def2;

            (b * a) = (( multR (x,v)) . (x1i,a1)) by Def8

            .= ( multR (x1i,a1)) by Def7

            .= (the multF of F . (xi,x)) by A1, A8, A5, Def6

            .= ( 1. ( ExField (x,v))) by A2, Def8;

            hence a is left_invertible by ALGSTR_0:def 27;

          end;

        end;

          suppose

           A9: a <> v;

          then not a in {v} by TARSKI:def 1;

          then

           A10: a in (( [#] F) \ {x}) by A3, XBOOLE_0:def 3;

          reconsider a1 = a as Element of ( carr (x,v)) by Def8;

          reconsider aR = a as Element of ( [#] F) by A10;

          aR <> ( 0. F) by A4, Def8;

          then

          consider aRi be Element of F such that

           A11: (aRi * aR) = ( 1. F) by ALGSTR_0:def 39, ALGSTR_0:def 27;

          per cases ;

            suppose

             A12: aRi = x;

            then

             A13: (the multF of F . (x,a)) <> x by A11, Def2;

            (u * a) = (( multR (x,v)) . (u1,a1)) by Def8

            .= ( multR (u1,a1)) by Def7

            .= (the multF of F . (aRi,aR)) by A13, A12, A9, Def6

            .= ( 1. ( ExField (x,v))) by A11, Def8;

            hence a is left_invertible by ALGSTR_0:def 27;

          end;

            suppose aRi <> x;

            then not aRi in {x} by TARSKI:def 1;

            then aRi in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider a1i = aRi as Element of ( carr (x,v)) by XBOOLE_0:def 3;

            reconsider b = a1i as Element of ( ExField (x,v)) by Def8;



             A14: (the multF of F . (b,a)) <> x by A11, Def2;



             A15: aR <> v & aRi <> v by A1;

            (b * a) = (( multR (x,v)) . (aRi,a1)) by Def8

            .= ( multR (a1i,a1)) by Def7

            .= (the multF of F . (aRi,aR)) by A15, A14, Def6

            .= ( 1. ( ExField (x,v))) by A11, Def8;

            hence a is left_invertible by ALGSTR_0:def 27;

          end;

        end;

      end;

      hence ( ExField (x,v)) is almost_left_invertible by ALGSTR_0:def 27;

    end;

    theorem :: FIELD_3:13



     Th13: for x be non trivial Element of F, P be Ring st P = ( ExField (x, <%( 0. F), ( 1. F)%>)) holds <%( 0. F), ( 1. F)%> in (( [#] P) /\ ( [#] ( Polynom-Ring P)))

    proof

      let x be non trivial Element of F, P be Ring;

      set C = ( carr (x, <%( 0. F), ( 1. F)%>)), E = ( ExField (x, <%( 0. F), ( 1. F)%>));

      assume

       A1: P = E;

       <%( 0. F), ( 1. F)%> in { <%( 0. F), ( 1. F)%>} by TARSKI:def 1;

      then <%( 0. F), ( 1. F)%> in C by XBOOLE_0:def 3;

      then

       A2: <%( 0. F), ( 1. F)%> in ( [#] E) by Def8;

      now

        let n be Element of NAT ;

        per cases by NAT_1: 23;

          suppose

           A3: n = 0 ;



          hence ( <%( 0. F), ( 1. F)%> . n) = ( 0. F) by POLYNOM5: 38

          .= ( 0. E) by Def8

          .= ( <%( 0. E), ( 1. E)%> . n) by A3, POLYNOM5: 38;

        end;

          suppose

           A4: n = 1;



          hence ( <%( 0. F), ( 1. F)%> . n) = ( 1. F) by POLYNOM5: 38

          .= ( 1. E) by Def8

          .= ( <%( 0. E), ( 1. E)%> . n) by A4, POLYNOM5: 38;

        end;

          suppose

           A5: n >= 2;



          hence ( <%( 0. F), ( 1. F)%> . n) = ( 0. F) by POLYNOM5: 38

          .= ( 0. E) by Def8

          .= ( <%( 0. E), ( 1. E)%> . n) by A5, POLYNOM5: 38;

        end;

      end;

      then <%( 0. F), ( 1. F)%> = <%( 0. E), ( 1. E)%>;

      then <%( 0. F), ( 1. F)%> in ( [#] ( Polynom-Ring P)) by A1, POLYNOM3:def 10;

      hence thesis by A1, A2, XBOOLE_0:def 4;

    end;

    theorem :: FIELD_3:14



     Th14: ex K be Field st (( [#] K) /\ ( [#] ( Polynom-Ring K))) <> {}

    proof

      set F = the non almost_trivial Field;

      set x = the non trivial Element of F;

      reconsider o = <%( 0. F), ( 1. F)%> as object;

      per cases ;

        suppose not o in ( [#] F);

        then

        reconsider K = ( ExField (x,o)) as Field by Th7, Th8, Th10, Th9, Th12, Th11;

        take K;

        thus thesis by Th13;

      end;

        suppose

         A1: ex a be Element of F st a = <%( 0. F), ( 1. F)%>;

        take F;

         <%( 0. F), ( 1. F)%> in ( [#] ( Polynom-Ring F)) by POLYNOM3:def 10;

        hence thesis by A1, XBOOLE_0:def 4;

      end;

    end;

    reserve n for non zero Nat;

    theorem :: FIELD_3:15

    ex K be Field, p be Polynomial of K st ( deg p) = n & p in (( [#] K) /\ ( [#] ( Polynom-Ring K)))

    proof

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

      set F = the non almost_trivial Field;

      set x = the non trivial Element of F;

      reconsider o = ( rpoly (n,( 0. F))) as object;

      per cases ;

        suppose not o in ( [#] F);

        then

        reconsider K = ( ExField (x,o)) as Field by Th7, Th8, Th10, Th9, Th12, Th11;

        set p = ( rpoly (n,( 0. K)));

        now

          let i be Element of NAT ;

          per cases ;

            suppose

             A1: i = 0 ;



            hence (( rpoly (n,( 0. F))) . i) = ( - (( power F) . (( 0. F),n))) by HURWITZ: 25

            .= ( - ( 0. F)) by Th6

            .= ( - ( 0. K)) by Def8

            .= ( - (( power K) . (( 0. K),n))) by Th6

            .= (p . i) by A1, HURWITZ: 25;

          end;

            suppose

             A2: i = n;



            hence (( rpoly (n,( 0. F))) . i) = ( 1_ F) by HURWITZ: 25

            .= ( 1_ K) by Def8

            .= (p . i) by A2, HURWITZ: 25;

          end;

            suppose

             A3: i <> 0 & i <> n;



            hence (( rpoly (n,( 0. F))) . i) = ( 0. F) by HURWITZ: 26

            .= ( 0. K) by Def8

            .= (p . i) by A3, HURWITZ: 26;

          end;

        end;

        then

         A4: ( rpoly (n,( 0. F))) = ( rpoly (n,( 0. K)));

        take K;

        take p = ( rpoly (n,( 0. K)));



         A5: p in ( [#] ( Polynom-Ring K)) by POLYNOM3:def 10;

        p in {( rpoly (n,( 0. F)))} by A4, TARSKI:def 1;

        then p in ( carr (x,( rpoly (n,( 0. F))))) by XBOOLE_0:def 3;

        then p in ( [#] K) by Def8;

        hence thesis by A5, XBOOLE_0:def 4, HURWITZ: 27;

      end;

        suppose

         A6: ex a be Element of F st a = ( rpoly (n,( 0. F)));

        take F;

        take x = ( rpoly (n,( 0. F)));

        x in ( [#] ( Polynom-Ring F)) by POLYNOM3:def 10;

        hence thesis by A6, HURWITZ: 27, XBOOLE_0:def 4;

      end;

    end;

    theorem :: FIELD_3:16

    ex K be Field, x be object st not x in ( rng ( canHom K)) & x in (( [#] K) /\ ( [#] ( Polynom-Ring K)))

    proof

      set F = the non almost_trivial Field;

      set y = the non trivial Element of F;

      reconsider o = <%( 0. F), ( 1. F)%> as object;

      per cases ;

        suppose not o in ( [#] F);

        then

        reconsider K = ( ExField (y,o)) as Field by Th7, Th8, Th10, Th9, Th12, Th11;

        take K;

        take x = <%( 0. K), ( 1. K)%>;

        now

          let n be Element of NAT ;

          per cases by NAT_1: 23;

            suppose

             A1: n = 0 ;



            hence ( <%( 0. F), ( 1. F)%> . n) = ( 0. F) by POLYNOM5: 38

            .= ( 0. K) by Def8

            .= ( <%( 0. K), ( 1. K)%> . n) by A1, POLYNOM5: 38;

          end;

            suppose

             A2: n = 1;



            hence ( <%( 0. F), ( 1. F)%> . n) = ( 1. F) by POLYNOM5: 38

            .= ( 1. K) by Def8

            .= ( <%( 0. K), ( 1. K)%> . n) by A2, POLYNOM5: 38;

          end;

            suppose

             A3: n >= 2;



            hence ( <%( 0. F), ( 1. F)%> . n) = ( 0. F) by POLYNOM5: 38

            .= ( 0. K) by Def8

            .= ( <%( 0. K), ( 1. K)%> . n) by A3, POLYNOM5: 38;

          end;

        end;

        then

         A4: <%( 0. F), ( 1. F)%> = <%( 0. K), ( 1. K)%>;

        then x in (( [#] K) /\ ( [#] ( Polynom-Ring K))) by Th13;

        then

        reconsider x as Element of the carrier of ( Polynom-Ring K);



         A5: ( deg x) = (( len x) - 1) by HURWITZ:def 2

        .= (2 - 1) by POLYNOM5: 40;

        now

          assume x in ( rng ( canHom K));

          then

          consider a be object such that

           A6: a in ( dom ( canHom K)) & x = (( canHom K) . a) by FUNCT_1:def 3;

          reconsider a as Element of ( [#] K) by A6;

          ( deg (a | K)) <= 0 by RATFUNC1:def 2;

          hence contradiction by A6, A5, RING_4:def 6;

        end;

        hence thesis by A4, Th13;

      end;

        suppose

         A7: ex a be Element of F st a = <%( 0. F), ( 1. F)%>;

        take F;

        take x = <%( 0. F), ( 1. F)%>;

        2 = ( len x) by POLYNOM5: 40;

        then

         A8: ( deg x) = (2 - 1) by HURWITZ:def 2;



         A9: x in the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        now

          assume x in ( rng ( canHom F));

          then

          consider a be object such that

           A10: a in ( dom ( canHom F)) & x = (( canHom F) . a) by FUNCT_1:def 3;

          reconsider a as Element of ( [#] F) by A10;

          ( deg (a | F)) <= 0 by RATFUNC1:def 2;

          hence contradiction by A10, A8, RING_4:def 6;

        end;

        hence thesis by A7, A9, XBOOLE_0:def 4;

      end;

    end;

    registration

      cluster non polynomial_disjoint for Field;

      existence

      proof

        consider F be Field such that

         A1: (( [#] F) /\ ( [#] ( Polynom-Ring F))) <> {} by Th14;

        take F;

        thus thesis by A1;

      end;

    end

    definition

      let F be non almost_trivial Field;

      let x be non trivial Element of F;

      let o be object;

      :: FIELD_3:def10

      func isoR (x,o) -> Function of F, ( ExField (x,o)) means

      : Def9: (it . x) = o & for a be Element of F st a <> x holds (it . a) = a;

      existence

      proof



         A1: ( [#] ( ExField (x,o))) = ( carr (x,o)) by Def8;

        defpred P[ object, object] means ($1 = x & $2 = o) or ($1 <> x & $2 = $1);



         A2: for u be object st u in ( [#] F) holds ex y be object st y in the carrier of ( ExField (x,o)) & P[u, y]

        proof

          let u be object;

          assume

           A3: u in ( [#] F);

          per cases ;

            suppose

             A4: u = x;

            take b = o;

            o in {o} by TARSKI:def 1;

            hence b in the carrier of ( ExField (x,o)) by A1, XBOOLE_0:def 3;

            thus thesis by A4;

          end;

            suppose

             A5: u <> x;

            take u;

             not u in {x} by A5, TARSKI:def 1;

            then u in (( [#] F) \ {x}) by A3, XBOOLE_0:def 5;

            hence u in the carrier of ( ExField (x,o)) by A1, XBOOLE_0:def 3;

            thus thesis by A5;

          end;

        end;

        consider g be Function of ( [#] F), the carrier of ( ExField (x,o)) such that

         A6: for u be object st u in ( [#] F) holds P[u, (g . u)] from FUNCT_2:sch 1( A2);

        reconsider g as Function of F, ( ExField (x,o));

        take g;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let g1,g2 be Function of F, ( ExField (x,o));

        assume that

         A7: (g1 . x) = o & for a be Element of F st a <> x holds (g1 . a) = a and

         A8: (g2 . x) = o & for a be Element of F st a <> x holds (g2 . a) = a;

        now

          let o be object;

          assume o in ( [#] F);

          then

          reconsider a = o as Element of F;

          per cases ;

            suppose a = x;

            hence (g1 . o) = (g2 . o) by A8, A7;

          end;

            suppose

             A9: a <> x;



            then (g1 . a) = a by A7

            .= (g2 . a) by A9, A8;

            hence (g1 . o) = (g2 . o);

          end;

        end;

        hence g1 = g2;

      end;

    end

    registration

      let F be non almost_trivial Field;

      let x be non trivial Element of F;

      let o be object;

      cluster ( isoR (x,o)) -> onto;

      coherence

      proof

        set f = ( isoR (x,o));



         A1: the carrier of ( ExField (x,o)) = ( carr (x,o)) by Def8;



         A2: ( rng f) c= the carrier of ( ExField (x,o)) by RELAT_1:def 19;

        now

          let u be object;

          assume

           A3: u in the carrier of ( ExField (x,o));

          per cases ;

            suppose o = u;

            then

             A4: (f . x) = u by Def9;

            ( [#] F) = ( dom f) by FUNCT_2:def 1;

            hence u in ( rng f) by A4, FUNCT_1:def 3;

          end;

            suppose o <> u;

            then not u in {o} by TARSKI:def 1;

            then

             A5: u in (( [#] F) \ {x}) by A3, A1, XBOOLE_0:def 3;

            then

            reconsider a = u as Element of F;

             not u in {x} by A5, XBOOLE_0:def 5;

            then x <> u by TARSKI:def 1;

            then

             A6: (f . a) = a by Def9;

            ( [#] F) = ( dom f) by FUNCT_2:def 1;

            hence u in ( rng f) by A6, FUNCT_1:def 3;

          end;

        end;

        hence f is onto by A2, TARSKI: 2;

      end;

    end

    theorem :: FIELD_3:17

    for x be non trivial Element of F, o be object st not o in ( [#] F) holds ( isoR (x,o)) is one-to-one

    proof

      let x be non trivial Element of F;

      let o be object;

      assume not o in ( [#] F);

      then

       A1: a <> o;

      set f = ( isoR (x,o));

      now

        let x1,x2 be object;

        assume

         A2: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        per cases ;

          suppose

           A3: x1 = x;

          now

            assume

             A4: x2 <> x;

            reconsider a = x2 as Element of F by A2;

            a = (f . a) by A4, Def9

            .= o by A3, A2, Def9;

            hence contradiction by A1;

          end;

          hence x1 = x2 by A3;

        end;

          suppose

           A5: x1 <> x;

          reconsider a = x1 as Element of F by A2;



           A6: (f . a) = a by A5, Def9;

          now

            assume

             A7: x2 <> x1;

            per cases ;

              suppose x2 = x;

              hence contradiction by A6, A1, A2, Def9;

            end;

              suppose

               A8: x2 <> x;

              reconsider b = x2 as Element of F by A2;

              thus contradiction by A2, A6, A8, A7, Def9;

            end;

          end;

          hence x1 = x2;

        end;

      end;

      hence f is one-to-one;

    end;

    theorem :: FIELD_3:18



     Th15: for x be non trivial Element of F, u be object st not u in ( [#] F) holds ( isoR (x,u)) is additive multiplicative unity-preserving

    proof

      let x be non trivial Element of F;

      let u be object;

      assume

       A1: not u in ( [#] F);

      then

       A2: a <> u;

      set f = ( isoR (x,u));

      u in {u} by TARSKI:def 1;

      then

      reconsider o = u as Element of ( carr (x,u)) by XBOOLE_0:def 3;

      now

        let a,b be Element of F;



         A3: a <> u & b <> u by A2;

        per cases ;

          suppose

           A4: a = x;

          then

           A5: (f . a) = u by Def9;

          per cases ;

            suppose

             A6: b = x;

            then

             A7: (f . b) = u by Def9;

            per cases ;

              suppose

               A8: (the addF of F . (x,x)) <> x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (u,u)) by A5, A7, Def8

              .= ( addR (o,o)) by Def5

              .= (a + b) by A4, A6, A8, Def4

              .= (f . (a + b)) by A4, A6, A8, Def9;

            end;

              suppose

               A9: (the addF of F . (x,x)) = x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (u,u)) by A5, A7, Def8

              .= ( addR (o,o)) by Def5

              .= u by A9, Def4

              .= (f . (a + b)) by A4, A6, A9, Def9;

            end;

          end;

            suppose

             A10: b <> x;

            then not b in {x} by TARSKI:def 1;

            then b in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider b1 = b as Element of ( carr (x,u)) by XBOOLE_0:def 3;



             A11: (f . b) = b by A10, Def9;

            per cases ;

              suppose

               A12: (the addF of F . (x,b)) <> x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (u,b)) by A5, A11, Def8

              .= ( addR (o,b1)) by Def5

              .= (a + b) by A2, A4, A12, Def4

              .= (f . (a + b)) by A4, A12, Def9;

            end;

              suppose

               A13: (the addF of F . (x,b)) = x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (u,b)) by A5, A11, Def8

              .= ( addR (o,b1)) by Def5

              .= u by A3, A13, Def4

              .= (f . (a + b)) by A4, A13, Def9;

            end;

          end;

        end;

          suppose

           A14: a <> x;

          then not a in {x} by TARSKI:def 1;

          then a in (( [#] F) \ {x}) by XBOOLE_0:def 5;

          then

          reconsider a1 = a as Element of ( carr (x,u)) by XBOOLE_0:def 3;



           A15: (f . a) = a by A14, Def9;

          per cases ;

            suppose

             A16: b = x;

            then

             A17: (f . b) = u by Def9;

            per cases ;

              suppose

               A18: (the addF of F . (a,x)) <> x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (a,u)) by A15, A17, Def8

              .= ( addR (a1,o)) by Def5

              .= (a + b) by A16, A2, A18, Def4

              .= (f . (a + b)) by A16, A18, Def9;

            end;

              suppose

               A19: (the addF of F . (a,x)) = x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (a,u)) by A15, A17, Def8

              .= ( addR (a1,o)) by Def5

              .= u by A3, A19, Def4

              .= (f . (a + b)) by A16, A19, Def9;

            end;

          end;

            suppose

             A20: b <> x;

            then not b in {x} by TARSKI:def 1;

            then b in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider b1 = b as Element of ( carr (x,u)) by XBOOLE_0:def 3;



             A21: (f . b) = b by A20, Def9;

            per cases ;

              suppose

               A22: (the addF of F . (a,b)) <> x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (a,b)) by A15, A21, Def8

              .= ( addR (a1,b1)) by Def5

              .= (a + b) by A3, A22, Def4

              .= (f . (a + b)) by A22, Def9;

            end;

              suppose

               A23: (the addF of F . (a,b)) = x;



              thus ((f . a) + (f . b)) = (( addR (x,u)) . (a,b)) by A15, A21, Def8

              .= ( addR (a1,b1)) by Def5

              .= u by A3, A23, Def4

              .= (f . (a + b)) by A23, Def9;

            end;

          end;

        end;

      end;

      hence f is additive;

      now

        let a,b be Element of F;



         A24: a <> u & b <> u by A1;

        per cases ;

          suppose

           A25: a = x;

          then

           A26: (f . a) = u by Def9;

          per cases ;

            suppose

             A27: b = x;

            then

             A28: (f . b) = u by Def9;

            per cases ;

              suppose

               A29: (the multF of F . (x,x)) <> x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (u,u)) by A26, A28, Def8

              .= ( multR (o,o)) by Def7

              .= (a * b) by A25, A27, A29, Def6

              .= (f . (a * b)) by A25, A27, A29, Def9;

            end;

              suppose

               A30: (the multF of F . (x,x)) = x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (u,u)) by A26, A28, Def8

              .= ( multR (o,o)) by Def7

              .= u by A30, Def6

              .= (f . (a * b)) by A25, A27, A30, Def9;

            end;

          end;

            suppose

             A31: b <> x;

            then not b in {x} by TARSKI:def 1;

            then b in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider b1 = b as Element of ( carr (x,u)) by XBOOLE_0:def 3;



             A32: (f . b) = b by A31, Def9;

            per cases ;

              suppose

               A33: (the multF of F . (x,b)) <> x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (u,b)) by A26, A32, Def8

              .= ( multR (o,b1)) by Def7

              .= (a * b) by A2, A25, A33, Def6

              .= (f . (a * b)) by A25, A33, Def9;

            end;

              suppose

               A34: (the multF of F . (x,b)) = x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (u,b)) by A26, A32, Def8

              .= ( multR (o,b1)) by Def7

              .= u by A24, A34, Def6

              .= (f . (a * b)) by A25, A34, Def9;

            end;

          end;

        end;

          suppose

           A35: a <> x;

          then not a in {x} by TARSKI:def 1;

          then a in (( [#] F) \ {x}) by XBOOLE_0:def 5;

          then

          reconsider a1 = a as Element of ( carr (x,u)) by XBOOLE_0:def 3;



           A36: (f . a) = a by A35, Def9;

          per cases ;

            suppose

             A37: b = x;

            then

             A38: (f . b) = u by Def9;

            per cases ;

              suppose

               A39: (the multF of F . (a,x)) <> x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (a,u)) by A36, A38, Def8

              .= ( multR (a1,o)) by Def7

              .= (a * b) by A2, A37, A39, Def6

              .= (f . (a * b)) by A37, A39, Def9;

            end;

              suppose

               A40: (the multF of F . (a,x)) = x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (a,u)) by A36, A38, Def8

              .= ( multR (a1,o)) by Def7

              .= u by A24, A40, Def6

              .= (f . (a * b)) by A37, A40, Def9;

            end;

          end;

            suppose

             A41: b <> x;

            then not b in {x} by TARSKI:def 1;

            then b in (( [#] F) \ {x}) by XBOOLE_0:def 5;

            then

            reconsider b1 = b as Element of ( carr (x,u)) by XBOOLE_0:def 3;



             A42: (f . b) = b by A41, Def9;

            per cases ;

              suppose

               A43: (the multF of F . (a,b)) <> x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (a,b)) by A36, A42, Def8

              .= ( multR (a1,b1)) by Def7

              .= (a * b) by A24, A43, Def6

              .= (f . (a * b)) by A43, Def9;

            end;

              suppose

               A44: (the multF of F . (a,b)) = x;



              thus ((f . a) * (f . b)) = (( multR (x,u)) . (a,b)) by A36, A42, Def8

              .= ( multR (a1,b1)) by Def7

              .= u by A24, A44, Def6

              .= (f . (a * b)) by A44, Def9;

            end;

          end;

        end;

      end;

      hence f is multiplicative by GROUP_6:def 6;

      reconsider S = ( ExField (x,u)) as well-unital Ring by A1, Th7, Th10, Th8, Th9, Th11;

      ( 1. F) <> x by Def2;



      then (f . ( 1_ F)) = ( 1. F) by Def9

      .= ( 1_ S) by Def8;

      hence f is unity-preserving;

    end;

    theorem :: FIELD_3:19

    for F be non almost_trivial Field holds ex K be non polynomial_disjoint Field st (K,F) are_isomorphic

    proof

      let F be non almost_trivial Field;

      set x = the non trivial Element of F;

      reconsider o = <%( 0. F), ( 1. F)%> as object;

      per cases ;

        suppose

         A1: not o in ( [#] F);

        then

        reconsider S = ( ExField (x,o)) as Field by Th7, Th8, Th9, Th10, Th11, Th12;

        (( [#] S) /\ ( [#] ( Polynom-Ring S))) <> {} by Th13;

        then

        reconsider S as non polynomial_disjoint Field by Def3;

        take S;

        ( isoR (x,o)) is additive multiplicative unity-preserving by A1, Th15;

        hence thesis by MOD_4:def 12, QUOFIELD:def 23;

      end;

        suppose ex a be Element of F st a = <%( 0. F), ( 1. F)%>;

        then

        consider a be Element of F such that

         A2: a = <%( 0. F), ( 1. F)%>;

        a in ( [#] ( Polynom-Ring F)) by A2, POLYNOM3:def 10;

        then a in (( [#] F) /\ ( [#] ( Polynom-Ring F))) by XBOOLE_0:def 4;

        then

        reconsider S = F as non polynomial_disjoint Field by Def3;

        take S;

        thus thesis;

      end;

    end;

    theorem :: FIELD_3:20

    for F be non almost_trivial Field holds ex K be non polynomial_disjoint Field, p be Polynomial of K st (K,F) are_isomorphic & ( deg p) = n & p in (( [#] K) /\ ( [#] ( Polynom-Ring K)))

    proof

      let F be non almost_trivial Field;

      set x = the non trivial Element of F;

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

      reconsider o = ( rpoly (n,( 0. F))) as object;

      set x = the non trivial Element of F;

      per cases ;

        suppose

         A1: not o in ( [#] F);

        then

        reconsider K = ( ExField (x,( rpoly (n,( 0. F))))) as Field by Th7, Th8, Th10, Th9, Th12, Th11;

        set p = ( rpoly (n,( 0. K)));

        now

          let i be Element of NAT ;

          per cases ;

            suppose

             A2: i = 0 ;



            hence (( rpoly (n,( 0. F))) . i) = ( - (( power F) . (( 0. F),n))) by HURWITZ: 25

            .= ( - ( 0. F)) by Th6

            .= ( - ( 0. K)) by Def8

            .= ( - (( power K) . (( 0. K),n))) by Th6

            .= (p . i) by A2, HURWITZ: 25;

          end;

            suppose

             A3: i = n;



            hence (( rpoly (n,( 0. F))) . i) = ( 1_ F) by HURWITZ: 25

            .= ( 1_ K) by Def8

            .= (p . i) by A3, HURWITZ: 25;

          end;

            suppose

             A4: i <> 0 & i <> n;



            hence (( rpoly (n,( 0. F))) . i) = ( 0. F) by HURWITZ: 26

            .= ( 0. K) by Def8

            .= (p . i) by A4, HURWITZ: 26;

          end;

        end;

        then

         A5: ( rpoly (n,( 0. F))) = ( rpoly (n,( 0. K)));



         A6: p in ( [#] ( Polynom-Ring K)) by POLYNOM3:def 10;

        p in {( rpoly (n,( 0. F)))} by A5, TARSKI:def 1;

        then p in ( carr (x,( rpoly (n,( 0. F))))) by XBOOLE_0:def 3;

        then

         A7: p in ( [#] K) by Def8;

        then p in (( [#] K) /\ ( [#] ( Polynom-Ring K))) by A6, XBOOLE_0:def 4;

        then

        reconsider K as non polynomial_disjoint Field by Def3;

        take K;

        take p = ( rpoly (n,( 0. K)));

        ( isoR (x,( rpoly (n,( 0. F))))) is additive multiplicative unity-preserving by A1, Th15;

        hence (K,F) are_isomorphic by MOD_4:def 12, QUOFIELD:def 23;

        thus thesis by A7, A6, XBOOLE_0:def 4, HURWITZ: 27;

      end;

        suppose

         A8: ex a be Element of F st a = ( rpoly (n,( 0. F)));

        then

        consider a be Element of F such that

         A9: a = ( rpoly (n,( 0. F)));

        a in the carrier of ( Polynom-Ring F) by A9, POLYNOM3:def 10;

        then a in (( [#] F) /\ ( [#] ( Polynom-Ring F))) by XBOOLE_0:def 4;

        then

        reconsider K = F as non polynomial_disjoint Field by Def3;

        take K;

        take x = ( rpoly (n,( 0. K)));

        x in the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        hence thesis by A8, HURWITZ: 27, XBOOLE_0:def 4;

      end;

    end;

    begin

    definition

      let R be Ring;

      :: FIELD_3:def11

      attr R is flat means

      : Def10: for a,b be Element of R holds ( the_rank_of a) = ( the_rank_of b);

    end

    registration

      cluster flat for Ring;

      existence

      proof

        set R = the trivial Ring;

        take R;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    theorem :: FIELD_3:21



     Th16: for R be flat Ring, p be Polynomial of R holds not p in ( [#] R)

    proof

      let R be flat Ring, p be Polynomial of R;

      now

        assume

         A1: p in ( [#] R);

        then

        reconsider a = p as Element of R;



         A2: ( the_rank_of p) = ( the_rank_of (p . 0 )) by A1, Def10;

        ( dom p) = NAT by FUNCT_2:def 1;

        then

         A3: [ 0 , (p . 0 )] in p by FUNCT_1:def 2;

        ( the_rank_of (p . 0 )) in ( the_rank_of [ 0 , (p . 0 )]) by CLASSES1: 84;

        hence contradiction by A2, A3, CLASSES1: 68;

      end;

      hence thesis;

    end;

    registration

      cluster -> polynomial_disjoint for flat Ring;

      coherence

      proof

        let R be flat Ring;

        set M = (( [#] R) /\ ( [#] ( Polynom-Ring R)));

        set x = the Element of M;

        now

          assume R is non polynomial_disjoint;

          then

           A1: x in ( [#] R) & x in ( [#] ( Polynom-Ring R)) by XBOOLE_0:def 4;

          then

          reconsider p = x as Polynomial of R by POLYNOM3:def 10;

          p = x;

          hence contradiction by A1, Th16;

        end;

        hence thesis;

      end;

    end

    theorem :: FIELD_3:22



     Th17: for R be non degenerated Ring st 0 in the carrier of R holds R is non flat

    proof

      let R be non degenerated Ring;



       A1: ( the_rank_of 0 ) = 0 by CLASSES1: 71;

      assume

       A2: 0 in the carrier of R;

      per cases ;

        suppose 0 = ( 0. R);

        then ( the_rank_of ( 1. R)) <> {} by CLASSES1: 71;

        hence R is non flat by A1, A2;

      end;

        suppose 0 = ( 1. R);

        then ( the_rank_of ( 0. R)) <> {} by CLASSES1: 71;

        hence R is non flat by A1, A2;

      end;

        suppose 0 <> ( 0. R) & 0 <> ( 1. R);

        then ( the_rank_of ( 0. R)) <> {} by CLASSES1: 71;

        hence R is non flat by A1, A2;

      end;

    end;

    registration

      cluster INT.Ring -> non flat;

      coherence by INT_3:def 3, Th17;

      cluster F_Rat -> non flat;

      coherence by GAUSSINT:def 14, Th17;

      cluster F_Real -> non flat;

      coherence by Th17;

    end

    registration

      let n be non trivial Nat;

      cluster ( Z/ n) -> non flat;

      coherence

      proof

        1 < n by NAT_2: 19, NAT_2:def 1;

        then ( 0. ( Z/ n)) = 0 by Th4;

        hence thesis by Th17;

      end;

    end

    begin

    theorem :: FIELD_3:23



     Th18: for R be Ring, p be Polynomial of R holds for n be Nat holds p <> n

    proof

      let R be Ring, p be Polynomial of R;

      let u be Nat;

      reconsider n = u as Element of NAT by ORDINAL1:def 12;

      now

        assume

         A1: p = n;

        ( dom p) = NAT by FUNCT_2:def 1;

        then

        consider i be Nat such that

         A2: i = [n, (p . n)] & i < n by A1;

        thus contradiction by A2;

      end;

      hence thesis;

    end;

    registration

      let n be non trivial Nat;

      cluster ( Z/ n) -> polynomial_disjoint;

      coherence

      proof

        ( Z/ n) = doubleLoopStr (# ( Segm n), ( addint n), ( multint n), ( In (1,( Segm n))), ( In ( 0 ,( Segm n))) #) by INT_3:def 12;

        then

         A1: ( [#] ( Z/ n)) = n by ORDINAL1:def 17;

        set M = (( [#] ( Z/ n)) /\ ( [#] ( Polynom-Ring ( Z/ n))));

        set x = the Element of M;

        now

          assume ( Z/ n) is non polynomial_disjoint;

          then

           A2: x in ( [#] ( Z/ n)) & x in ( [#] ( Polynom-Ring ( Z/ n))) by XBOOLE_0:def 4;

          then

          reconsider p = x as Polynomial of ( Z/ n) by POLYNOM3:def 10;

          x in { m where m be Nat : m < n } by A1, A2, Th1;

          then

          consider m be Nat such that

           A3: x = m & m < n;

          m = p by A3;

          hence contradiction by Th18;

        end;

        hence thesis;

      end;

    end

    registration

      cluster polynomial_disjoint for finite Field;

      existence

      proof

        take ( Z/ 2);

        2 is non trivial by NAT_2:def 1;

        hence thesis;

      end;

    end

    theorem :: FIELD_3:24



     Th19: for R be Ring, p be Polynomial of R holds for i be Integer holds p <> i

    proof

      let R be Ring, p be Polynomial of R;

      let i be Integer;



       A1: i in INT by INT_1:def 2;

      now

        assume

         A2: p = i;

        per cases by A1, NUMBERS:def 4, XBOOLE_0:def 3;

          suppose i in NAT ;

          then

          reconsider n = i as Element of NAT ;

          p = n by A2;

          hence contradiction by Th18;

        end;

          suppose i in [: { 0 }, NAT :];

          then

          consider x,y be object such that

           A3: x in { 0 } & y in NAT & i = [x, y] by ZFMISC_1:def 2;

          reconsider n = y as Element of NAT by A3;



           A4: p = [ 0 , n] by A2, A3, TARSKI:def 1

          .= { { 0 , n}, { 0 }} by TARSKI:def 5;



           A5: ( dom p) = NAT by FUNCT_2:def 1;

          per cases by A4, A5;

            suppose

             A6: [ 0 , (p . 0 )] = { 0 , n};

             [ 0 , (p . 0 )] = { { 0 , (p . 0 )}, { 0 }} by TARSKI:def 5;

            then

             A7: 0 in { { 0 , (p . 0 )}, { 0 }} by A6, TARSKI:def 2;

            per cases by A7;

              suppose 0 = { 0 };

              hence contradiction by CARD_1: 49;

            end;

              suppose 0 = { 0 , (p . 0 )};

              then {} = { 0 , (p . 0 )};

              hence contradiction;

            end;

          end;

            suppose [ 0 , (p . 0 )] = { 0 };

            hence contradiction by CARD_1: 49;

          end;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster INT.Ring -> polynomial_disjoint;

      coherence

      proof

        set R = INT.Ring ;

        set M = (( [#] R) /\ ( [#] ( Polynom-Ring R)));

        set x = the Element of M;

        now

          assume R is non polynomial_disjoint;

          then x in ( [#] R) & x in ( [#] ( Polynom-Ring R)) by XBOOLE_0:def 4;

          then

          reconsider p = x as Polynomial of R by POLYNOM3:def 10;

          reconsider x as Integer;

          p = x;

          hence contradiction by Th19;

        end;

        hence thesis;

      end;

    end



     Lem2: for R be Ring, p be Polynomial of R holds for r be Rational holds r in RAT+ & p = r implies r = [1, 2]

    proof

      let R be Ring, p be Polynomial of R;

      let r be Rational;

      assume

       A1: r in RAT+ & p = r;



       A2: ( dom p) = NAT by FUNCT_2:def 1;

       not r in omega by A1, Th19;

      then r in ({ [i, j] where i,j be Element of omega : (i,j) are_coprime & j <> {} } \ the set of all [k, 1] where k be Element of omega ) by A1, XBOOLE_0:def 3;

      then

       A3: r in { [i, j] where i,j be Element of omega : (i,j) are_coprime & j <> {} } & not r in the set of all [k, 1] where k be Element of omega by XBOOLE_0:def 5;

      then

      consider i,j be Element of omega such that

       A4: r = [i, j] & (i,j) are_coprime & j <> {} ;

       [i, (p . i)] in p by A2, FUNCT_1:def 2;

      then { {i, (p . i)}, {i}} in p by TARSKI:def 5;

      then

       A5: { {i, (p . i)}, {i}} in { {i, j}, {i}} by A1, A4, TARSKI:def 5;

      per cases by A5, TARSKI:def 2;

        suppose

         A6: { {i, (p . i)}, {i}} = {i, j};



         A7: j in {i, j} by TARSKI:def 2;

        per cases by A6, A7, TARSKI:def 2;

          suppose j = {i};

          then i = 0 by Th2;

          then j = 1 by A4, ARYTM_3: 3;

          hence r = [1, 2] by A3, A4;

        end;

          suppose

           A8: j = {i, (p . i)};

          per cases ;

            suppose i = (p . i);

            then for o be object holds o in j iff o = i by A8, TARSKI:def 2;

            then j = {i} by TARSKI:def 1;

            then i = {} by Th2;

            then j = 1 by A4, ARYTM_3: 3;

            hence r = [1, 2] by A3, A4;

          end;

            suppose i <> (p . i);

            per cases by A8, Th3;

              suppose i = 1 & (p . i) = 0 ;

              hence r = [1, 2] by A8, A4, CARD_1: 50;

            end;

              suppose i = 0 & (p . i) = 1;

              then j = 1 by A4, ARYTM_3: 3;

              hence r = [1, 2] by A3, A4;

            end;

          end;

        end;

      end;

        suppose

         A11: { {i, (p . i)}, {i}} = {i};

         {i, (p . i)} in { {i, (p . i)}, {i}} by TARSKI:def 2;

        then {i, (p . i)} = i by A11, TARSKI:def 1;

        then i in i by TARSKI:def 2;

        hence r = [1, 2];

      end;

    end;



     Lem3: for R be Ring, p be Polynomial of R holds p <> [1, 2]

    proof

      let R be Ring, p be Polynomial of R;



       A1: ( dom p) = NAT by FUNCT_2:def 1;

      now

        assume p = [1, 2];

        then

         A2: p = { {1, 2}, {1}} by TARSKI:def 5;

        per cases by A2, A1;

          suppose [3, (p . 3)] = {1, 2};

          then

           A3: { {3, (p . 3)}, {3}} = {1, 2} by TARSKI:def 5;



           A4: {3} in { {3, (p . 3)}, {3}} by TARSKI:def 2;

          per cases by A3, A4, TARSKI:def 2;

            suppose

             A5: 1 = {3};

            3 in {3} by TARSKI:def 1;

            hence contradiction by A5, CARD_1: 49, TARSKI:def 1;

          end;

            suppose

             A7: 2 = {3};



             A8: 3 in {3} by TARSKI:def 1;

            per cases by A7, A8, CARD_1: 50, TARSKI:def 2;

              suppose 3 = 0 ;

              hence contradiction;

            end;

              suppose 3 = 1;

              hence contradiction;

            end;

          end;

        end;

          suppose [3, (p . 3)] = {1};

          then

           A9: { {3, (p . 3)}, {3}} = {1} by TARSKI:def 5;

           {3} in { {3, (p . 3)}, {3}} by TARSKI:def 2;

          then

           A10: {3} = { 0 } by A9, TARSKI:def 1, CARD_1: 49;

          3 in {3} by TARSKI:def 1;

          hence contradiction by A10, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_3:25



     Th20: for R be Ring, p be Polynomial of R holds for r be Rational holds p <> r

    proof

      let R be Ring, p be Polynomial of R;

      let r be Rational;



       A1: r in (( RAT+ \/ [: { 0 }, RAT+ :]) \ { [ 0 , 0 ]}) by NUMBERS:def 3, RAT_1:def 2;

      now

        assume

         A2: p = r;

        then not r in RAT+ by Lem2, Lem3;

        then r in [: { 0 }, RAT+ :] by A1, XBOOLE_0:def 3;

        then

        consider x,y be object such that

         A3: x in { 0 } & y in RAT+ & r = [x, y] by ZFMISC_1:def 2;

        ( dom p) = NAT by FUNCT_2:def 1;

        then [1, (p . 1)] in p by FUNCT_1:def 2;

        then

         A4: [1, (p . 1)] in { {x, y}, {x}} by A3, A2, TARSKI:def 5;

        per cases by A4, TARSKI:def 2;

          suppose [1, (p . 1)] = {x, y};

          then

           A5: { {1, (p . 1)}, {1}} = {x, y} by TARSKI:def 5;



           A6: x in {x, y} by TARSKI:def 2;

          per cases by A5, A6, TARSKI:def 2;

            suppose x = {1, (p . 1)};

            hence contradiction by A3, TARSKI:def 1;

          end;

            suppose x = {1};

            hence contradiction by A3, TARSKI:def 1;

          end;

        end;

          suppose [1, (p . 1)] = {x};

          hence contradiction by A3, TARSKI:def 1, CARD_1: 49;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster F_Rat -> polynomial_disjoint;

      coherence

      proof

        set R = F_Rat , x = the Element of (( [#] R) /\ ( [#] ( Polynom-Ring R)));

        now

          assume R is non polynomial_disjoint;

          then

           A1: x in ( [#] R) & x in ( [#] ( Polynom-Ring R)) by XBOOLE_0:def 4;

          then

          reconsider p = x as Polynomial of R by POLYNOM3:def 10;

          reconsider x as Rational by A1;

          p = x;

          hence contradiction by Th20;

        end;

        hence thesis;

      end;

    end



     Lem4: for R be Ring, p be Polynomial of R holds for r be Real st r in REAL+ holds p <> r

    proof

      let R be Ring, p be Polynomial of R;

      let x be Real;

      assume

       A1: x in REAL+ ;



       A2: ( dom p) = NAT by FUNCT_2:def 1;

      then

       A3: [ 0 , (p . 0 )] in p & [1, (p . 1)] in p by FUNCT_1:def 2;

      now

        assume

         A4: p = x;

        per cases ;

          suppose x is Rational;

          hence contradiction by A4, Th20;

        end;

          suppose not x is Rational;

          then not x in RAT ;

          then ( not x in ( RAT+ \/ [: { 0 }, RAT+ :])) or x in { [ 0 , 0 ]} by NUMBERS:def 3, XBOOLE_0:def 5;

          per cases by XBOOLE_0:def 3;

            suppose

             A5: x in { [ 0 , 0 ]};

             [ 0 , 0 ] = { { 0 }, { 0 , 0 }} by TARSKI:def 5;

            hence contradiction by A2, A4, A5;

          end;

            suppose not x in RAT+ & not x in [: { 0 }, RAT+ :];

            then x in DEDEKIND_CUTS by A1, ARYTM_2:def 2, XBOOLE_0:def 3;

            then x in { A where A be Subset of RAT+ : for r be Element of RAT+ holds r in A implies (for s be Element of RAT+ st s <=' r holds s in A) & ex s be Element of RAT+ st s in A & r < s } & not x in { RAT+ } by ARYTM_2:def 1, XBOOLE_0:def 5;

            then

            consider A be Subset of RAT+ such that

             A6: x = A & for r be Element of RAT+ holds r in A implies (for s be Element of RAT+ st s <=' r holds s in A) & ex s be Element of RAT+ st s in A & r < s;

            consider u be Element of A such that

             A7: u = [ 0 , (p . 0 )] by A3, A4, A6;

            u in A by A4, A6;

            then

            reconsider u as Element of RAT+ ;

            per cases by XBOOLE_0:def 3;

              suppose u in omega ;

              then

              reconsider n = u as Element of omega ;

              n = {1, 1} by A7;

              hence contradiction by A7;

            end;

              suppose u in ({ [i, j] where i,j be Element of omega : (i,j) are_coprime & j <> {} } \ the set of all [k, 1] where k be Element of omega );

              then

               A8: u in { [i, j] where i,j be Element of omega : (i,j) are_coprime & j <> {} } & not u in the set of all [k, 1] where k be Element of omega by XBOOLE_0:def 5;

              then

              consider i,j be Element of omega such that

               A9: u = [i, j] & (i,j) are_coprime & j <> {} ;

              i = 0 by A7, A9, XTUPLE_0: 1;

              then j = 1 by A9, ARYTM_3: 3;

              hence contradiction by A8, A9;

            end;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FIELD_3:26



     Th21: for R be Ring, p be Polynomial of R holds for r be Real holds p <> r

    proof

      let R be Ring, p be Polynomial of R;

      let r be Real;



       A1: r in (( REAL+ \/ [: { 0 }, REAL+ :]) \ { [ 0 , 0 ]}) by XREAL_0:def 1, NUMBERS:def 1;

      now

        assume

         A2: p = r;

        then not r in REAL+ by Lem4;

        then r in [: { 0 }, REAL+ :] by A1, XBOOLE_0:def 3;

        then

        consider x,y be object such that

         A3: x in { 0 } & y in REAL+ & r = [x, y] by ZFMISC_1:def 2;

        ( dom p) = NAT by FUNCT_2:def 1;

        then [1, (p . 1)] in p by FUNCT_1:def 2;

        then

         A4: [1, (p . 1)] in { {x, y}, {x}} by A3, A2, TARSKI:def 5;

        per cases by A4, TARSKI:def 2;

          suppose [1, (p . 1)] = {x, y};

          then

           A5: { {1, (p . 1)}, {1}} = {x, y} by TARSKI:def 5;

          x in {x, y} by TARSKI:def 2;

          per cases by A5, TARSKI:def 2;

            suppose x = {1, (p . 1)};

            then x <> {} ;

            hence contradiction by A3, TARSKI:def 1;

          end;

            suppose x = {1};

            then x <> {} ;

            hence contradiction by A3, TARSKI:def 1;

          end;

        end;

          suppose [1, (p . 1)] = {x};

          hence contradiction by A3, TARSKI:def 1, CARD_1: 49;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster F_Real -> polynomial_disjoint;

      coherence

      proof

        set R = F_Real , x = the Element of (( [#] R) /\ ( [#] ( Polynom-Ring R)));

        now

          assume R is non polynomial_disjoint;

          then x in ( [#] R) & x in ( [#] ( Polynom-Ring R)) by XBOOLE_0:def 4;

          then

          reconsider p = x as Polynomial of R by POLYNOM3:def 10;

          reconsider x as Real;

          p = x;

          hence contradiction by Th21;

        end;

        hence thesis;

      end;

    end

    registration

      cluster polynomial_disjoint for infinite Field;

      existence

      proof

        take F_Rat ;

        thus thesis;

      end;

    end

    registration

      let R be polynomial_disjoint Ring;

      cluster ( Polynom-Ring R) -> polynomial_disjoint;

      coherence

      proof

        set RX = ( Polynom-Ring R), x = the Element of (( [#] RX) /\ ( [#] ( Polynom-Ring RX)));

        now

          assume RX is non polynomial_disjoint;

          then

           A1: x in ( [#] RX) & x in ( [#] ( Polynom-Ring RX)) by XBOOLE_0:def 4;

          then

          reconsider p1 = x as Polynomial of RX by POLYNOM3:def 10;

          reconsider p2 = x as Polynomial of R by A1, POLYNOM3:def 10;

          (p2 . 0 ) in ( [#] R);

          then (p1 . 0 ) in (( [#] R) /\ ( [#] ( Polynom-Ring R))) by XBOOLE_0:def 4;

          hence contradiction by Def3;

        end;

        hence thesis;

      end;

    end

    registration

      let F be Field, p be Element of ( [#] ( Polynom-Ring F));

      cluster (( Polynom-Ring F) / ( {p} -Ideal )) -> polynomial_disjoint;

      coherence

      proof

        set FX = ( Polynom-Ring F), I = ( {p} -Ideal );

        set K = (( Polynom-Ring F) / ( {p} -Ideal ));

        set x = the Element of (( [#] K) /\ ( [#] ( Polynom-Ring K)));

        now

          assume

           A1: K is non polynomial_disjoint;

          then

           A2: x in ( [#] K) & x in ( [#] ( Polynom-Ring K)) by XBOOLE_0:def 4;

          reconsider x as Element of K by A1, XBOOLE_0:def 4;

          reconsider q = x as Polynomial of K by A2, POLYNOM3:def 10;

          consider a be Element of FX such that

           A3: x = ( Class (( EqRel (FX,I)),a)) by RING_1: 11;

          reconsider p = a as Polynomial of F by POLYNOM3:def 10;

          for o be object st o in q holds ex n be Element of NAT , u be object st o = [n, u]

          proof

            let o be object;

            assume o in q;

            then

            consider a,b be object such that

             A4: a in NAT & b in ( [#] K) & o = [a, b] by ZFMISC_1:def 2;

            reconsider a as Element of NAT by A4;

            take a, b;

            thus thesis by A4;

          end;

          then

          consider n be Element of NAT , u be object such that

           A5: p = [n, u] by A3, EQREL_1: 20;

          ( dom p) = NAT by FUNCT_2:def 1;

          then [n, (p . n)] in p by FUNCT_1: 1;

          then

           A6: [n, (p . n)] in { {n}, {n, u}} by A5, TARSKI:def 5;

          now

            let a,b be object;

            assume [n, a] in { {n}, {n, b}};

            then

             A7: { {n}, {n, a}} in { {n}, {n, b}} by TARSKI:def 5;

            per cases by A7, TARSKI:def 2;

              suppose

               A8: { {n}, {n, a}} = {n};

               {n} in { {n}, {n, a}} by TARSKI:def 2;

              hence contradiction by A8;

            end;

              suppose

               A9: { {n}, {n, a}} = {n, b};



               A10: n in {n, b} by TARSKI:def 2;

              per cases by A10, A9, TARSKI:def 2;

                suppose n = {n};

                then n in n by TARSKI:def 1;

                hence contradiction;

              end;

                suppose n = {n, a};

                then n in n by TARSKI:def 2;

                hence contradiction;

              end;

            end;

          end;

          hence contradiction by A6;

        end;

        hence thesis;

      end;

    end

    registration

      let F be polynomial_disjoint Field;

      let p be non constant Element of the carrier of ( Polynom-Ring F);

      cluster ( Polynom-Ring p) -> polynomial_disjoint;

      coherence

      proof

        set RX = ( Polynom-Ring p), FX = ( Polynom-Ring F);

        set M = (( [#] RX) /\ ( [#] ( Polynom-Ring RX)));

        set x = the Element of M;



         A1: ( [#] RX) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

        now

          assume RX is non polynomial_disjoint;

          then

           A2: x in ( [#] RX) & x in ( [#] ( Polynom-Ring RX)) by XBOOLE_0:def 4;

          then

          consider q be Polynomial of F such that

           A3: x = q & ( deg q) < ( deg p) by A1;

          reconsider r = x as Polynomial of RX by A2, POLYNOM3:def 10;

          now

            let o be object;

            assume

             A4: o in ( rng r);

            ( rng r) c= ( [#] RX) by RELAT_1:def 19;

            then o in ( [#] RX) by A4;

            then

            consider u be Polynomial of F such that

             A5: o = u & ( deg u) < ( deg p) by A1;

            thus o in ( [#] FX) by A5, POLYNOM3:def 10;

          end;

          then ( rng r) c= ( [#] FX);

          then

          reconsider y = x as Function of NAT , FX by FUNCT_2: 6;

          ex n be Nat st for i be Nat st i >= n holds (y . i) = ( 0. FX)

          proof

            consider n be Nat such that

             A6: for i be Nat st i >= n holds (r . i) = ( 0. RX) by ALGSEQ_1:def 1;

            take n;

            now

              let i be Nat;

              assume i >= n;



              hence (y . i) = ( 0. RX) by A6

              .= ( 0_. F) by RING_4:def 8

              .= ( 0. FX) by POLYNOM3:def 10;

            end;

            hence thesis;

          end;

          then y is finite-Support by ALGSEQ_1:def 1;

          then

           A8: x in ( [#] ( Polynom-Ring FX)) by POLYNOM3:def 10;

          x in ( [#] ( Polynom-Ring F)) by A3, POLYNOM3:def 10;

          then x in (( [#] FX) /\ ( [#] ( Polynom-Ring FX))) by A8, XBOOLE_0:def 4;

          hence contradiction by Def3;

        end;

        hence thesis;

      end;

    end