field_5.miz



    begin

    theorem :: FIELD_5:1

    for X,Y be set st Y c= X holds ((X \ Y) \/ Y) = X

    proof

      let X,Y be set;

      assume

       AS: Y c= X;

       A:

      now

        let o be object;

        assume

         B: o in X;

        per cases ;

          suppose o in Y;

          hence o in ((X \ Y) \/ Y) by XBOOLE_0:def 3;

        end;

          suppose not o in Y;

          then o in (X \ Y) by B, XBOOLE_0:def 5;

          hence o in ((X \ Y) \/ Y) by XBOOLE_0:def 3;

        end;

      end;

      now

        let o be object;

        assume

         B: o in ((X \ Y) \/ Y);

        now

          assume

           C: not o in X;

          then not o in (X \ Y);

          then o in Y by B, XBOOLE_0:def 3;

          hence contradiction by AS, C;

        end;

        hence o in X;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: FIELD_5:2

    

     th0a: for n,m be Nat holds (n +` m) = (n + m) & (n *` m) = (n * m)

    proof

      let n,m be Nat;

      

      thus (n +` m) = (( card n) +` ( card m))

      .= ( card (n + m)) by CARD_2: 38

      .= (n + m);

      

      thus (n *` m) = ( card [:n, m:]) by CARD_2:def 2

      .= (( card n) * ( card m)) by CARD_2: 46

      .= (n * m);

    end;

    theorem :: FIELD_5:3

    

     th0k: for n,m be Nat holds (n c= m iff n <= m) & (n in m iff n < m)

    proof

      let n,m be Nat;

      

       H: n = ( Segm n) & m = ( Segm m);

       A:

      now

        assume n c= m;

        then ( card ( Segm n)) c= ( card ( Segm m));

        hence n <= m by NAT_1: 40;

      end;

      now

        assume n <= m;

        then ( card ( Segm n)) c= ( card ( Segm m)) by NAT_1: 40;

        hence n c= m;

      end;

      hence n c= m iff n <= m by A;

       A:

      now

        assume n in m;

        then ( card n) in ( card m);

        hence n < m by H, NAT_1: 41;

      end;

      now

        assume n < m;

        then ( card ( Segm n)) in ( card ( Segm m)) by NAT_1: 41;

        hence n in m;

      end;

      hence n in m iff n < m by A;

    end;

    theorem :: FIELD_5:4

    

     th0e: for n be Nat holds ( exp (2,n)) = (2 |^ n)

    proof

      let n be Nat;

      defpred P[ Nat] means ( exp (2,$1)) = (2 |^ $1);

      

       IA: P[ 0 ]

      proof

        

        thus ( exp (2, 0 )) = 1 by CARD_2: 25

        .= (2 |^ 0 ) by NEWTON: 4;

      end;

       IS:

      now

        let k be Nat;

        assume

         IV: P[k];

        ( exp (2,(k + 1))) = ( exp (2,(k +` 1))) by th0a

        .= (( exp (2,k)) *` ( exp (2,1))) by CARD_2: 28

        .= ((2 |^ k) *` 2) by IV, CARD_2: 27

        .= ((2 |^ k) * 2) by th0a

        .= (2 |^ (k + 1)) by NEWTON: 6;

        hence P[(k + 1)];

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      hence thesis;

    end;

    theorem :: FIELD_5:5

    

     th0n: for n be Nat st n >= 3 holds (n + n) < (2 |^ n)

    proof

      let n be Nat;

      assume

       AS: n >= 3;

      defpred P[ Nat] means ($1 + $1) < (2 |^ $1);

      

       IA: P[3]

      proof

        (2 |^ (2 + 1)) = ((2 |^ (1 + 1)) * 2) by NEWTON: 6

        .= (((2 |^ 1) * (2 |^ 1)) * 2) by NEWTON: 6

        .= ((2 * 2) * 2);

        hence (2 |^ 3) > (3 + 3);

      end;

       IS:

      now

        let k be Nat;

        assume

         A: k >= 3;

        assume

         B: P[k];

        

         C: (2 |^ (k + 1)) = ((2 |^ k) * 2) by NEWTON: 6

        .= ((2 |^ k) + (2 |^ k));

        

         D: ((2 |^ k) + (2 |^ k)) > ((k + k) + (k + k)) by B, XREAL_1: 8;

        k > 1 by A, XXREAL_0: 2;

        then (k + k) > (k + 1) by XREAL_1: 8;

        then ((k + k) + (k + k)) > ((k + 1) + (k + 1)) by XREAL_1: 8;

        hence P[(k + 1)] by C, D, XXREAL_0: 2;

      end;

      for k be Nat st k >= 3 holds P[k] from NAT_1:sch 8( IA, IS);

      hence thesis by AS;

    end;

    theorem :: FIELD_5:6

    

     th0b: for n be Nat st n >= 3 holds (n +` n) in ( exp (2,n))

    proof

      let n be Nat;

      assume

       AS: n >= 3;

      (n +` n) = (n + n) by th0a;

      then (n +` n) < (2 |^ n) by AS, th0n;

      then (n +` n) in (2 |^ n) by th0k;

      hence thesis by th0e;

    end;

    theorem :: FIELD_5:7

     NAT meets ( bool NAT )

    proof

       0 in NAT ;

      then { 0 } c= NAT by TARSKI:def 1;

      then ( NAT /\ ( bool NAT )) <> {} by CARD_1: 49, XBOOLE_0:def 4;

      hence thesis by XBOOLE_0:def 7;

    end;

    theorem :: FIELD_5:8

    

     th1: for X be set holds ex o be object st not o in X

    proof

      let X be set;

      now

        assume for u be object st u in ( bool X) holds u in X;

        then ( bool X) c= X;

        then

         B: ( card ( bool X)) c= ( card X) by CARD_1: 11;

        ( card X) in ( card ( bool X)) by CARD_1: 14;

        hence contradiction by B, CARD_1: 3;

      end;

      hence thesis;

    end;

    theorem :: FIELD_5:9

    

     thre: for X be set holds ex Y be set st ( card X) c= ( card Y) & (X /\ Y) = {}

    proof

      let X be set;

      set D = (( bool X) /\ X);

      set Y = (( bool X) \ (( bool X) /\ X));

       C:

      now

        assume

         H: (Y /\ X) <> {} ;

        set o = the Element of (Y /\ X);

        

         H1: o in Y & o in X by H, XBOOLE_0:def 4;

        then o in ( bool X) & not o in D by XBOOLE_0:def 5;

        hence contradiction by H1, XBOOLE_0:def 4;

      end;

      

       B: ( card ( bool X)) c= (( card Y) +` ( card X))

      proof

        now

          let o be object;

          assume

           B1: o in ( bool X);

          per cases ;

            suppose o in X;

            hence o in (Y \/ X) by XBOOLE_0:def 3;

          end;

            suppose not o in X;

            then not o in D by XBOOLE_0:def 4;

            then o in Y by B1, XBOOLE_0:def 5;

            hence o in (Y \/ X) by XBOOLE_0:def 3;

          end;

        end;

        then

         B1: ( bool X) c= (Y \/ X);

        ( card (Y \/ X)) = (( card Y) +` ( card X)) by C, CARD_2: 35, XBOOLE_0:def 7;

        hence thesis by B1, CARD_1: 11;

      end;

      per cases ;

        suppose

         AS: ( card X) = 0 ;

        set u = the object;

        take Y = {u};

        thus ( card X) c= ( card Y) by AS;

        now

          assume

           A: (X /\ Y) <> {} ;

          set o = the Element of (X /\ Y);

          o in X & o in Y by A, XBOOLE_0:def 4;

          hence contradiction by AS;

        end;

        hence thesis;

      end;

        suppose

         AS: ( card X) = 1;

        then

        consider o be object such that

         A: X = {o} by CARD_2: 42;

        consider u be object such that

         B: not u in {o} by th1;

        take Y = {u};

        thus ( card X) c= ( card Y) by AS, CARD_2: 42;

        now

          assume

           C: (X /\ Y) <> {} ;

          set x = the Element of (X /\ Y);

          x in X & x in Y by C, XBOOLE_0:def 4;

          hence contradiction by A, B, TARSKI:def 1;

        end;

        hence thesis;

      end;

        suppose

         AS: ( card X) = 2;

        then

        consider x,y be object such that

         A: x <> y & X = {x, y} by CARD_2: 60;

        consider u be object such that

         B: not u in {x, y} by th1;

        consider v be object such that

         C: not v in {x, y, u} by th1;

        take Y = {u, v};

        u <> v by C, ENUMSET1:def 1;

        hence ( card X) c= ( card Y) by AS, CARD_2: 57;

        now

          assume

           H: (X /\ Y) <> {} ;

          set o = the Element of (X /\ Y);

          

           E: o in X & o in Y by H, XBOOLE_0:def 4;

          then

           F: o = x or o = y by A, TARSKI:def 2;

          per cases by E, TARSKI:def 2;

            suppose o = u;

            hence contradiction by A, B, H, XBOOLE_0:def 4;

          end;

            suppose o = v;

            hence contradiction by F, C, ENUMSET1:def 1;

          end;

        end;

        hence thesis;

      end;

        suppose

         AS: ( card X) is finite & ( card X) <> 0 & ( card X) <> 1 & ( card X) <> 2;

        reconsider n = ( card X) as Nat by AS;

         D:

        now

          assume n < (2 + 1);

          then n <= 2 by NAT_1: 13;

          then n = 0 or ... or n = 2;

          hence contradiction by AS;

        end;

        

         B0: ( card ( bool X)) = ( exp (2,n)) by CARD_2: 31;

        now

          assume ( card Y) c= ( card X);

          then (( card Y) +` n) c= (n +` n) by CARD_2: 83;

          then ( card ( bool X)) c= (n +` n) by B;

          hence contradiction by D, B0, th0b, CARD_1: 4;

        end;

        hence thesis by C;

      end;

        suppose

         AS: not ( card X) is finite;

        now

          assume ( card Y) c= ( card X);

          then (( card Y) +` ( card X)) c= (( card X) +` ( card X)) by CARD_2: 83;

          then (( card Y) +` ( card X)) c= ( card X) by AS, CARD_2: 75;

          then ( card ( bool X)) c= ( card X) by B;

          hence contradiction by CARD_1: 4, CARD_1: 14;

        end;

        hence thesis by C;

      end;

    end;

    theorem :: FIELD_5:10

    

     thre1: for X,Y be set st ( card X) c= ( card Y) holds ex Z be set st Z c= Y & ( card Z) = ( card X)

    proof

      let X,Y be set;

      assume ( card X) c= ( card Y);

      then

      consider f be Function such that

       A: f is one-to-one & ( dom f) = X & ( rng f) c= Y by CARD_1: 10;

      take Z = ( rng f);

      thus thesis by A, CARD_1: 70;

    end;

    theorem :: FIELD_5:11

    for X be set holds ex Y be set st ( card X) = ( card Y) & (X /\ Y) = {}

    proof

      let X be set;

      consider Y be set such that

       A: ( card X) c= ( card Y) & (X /\ Y) = {} by thre;

      consider Z be set such that

       B: Z c= Y & ( card Z) = ( card X) by A, thre1;

      take Z;

      thus ( card X) = ( card Z) by B;

      now

        assume

         C: (X /\ Z) <> {} ;

        set o = the Element of (X /\ Z);

        o in X & o in Z by C, XBOOLE_0:def 4;

        hence contradiction by A, B, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: FIELD_5:12

    

     pr1: for E be Field, F be Subfield of E holds F is Subring of E

    proof

      let E be Field, F be Subfield of E;

      the carrier of F c= the carrier of E & the addF of F = (the addF of E || the carrier of F) & the multF of F = (the multF of E || the carrier of F) & ( 1. E) = ( 1. F) & ( 0. E) = ( 0. F) by EC_PF_1:def 1;

      hence thesis by C0SP1:def 3;

    end;

    theorem :: FIELD_5:13

    for F be Field, R be Subring of F holds R is Subfield of F iff R is Field

    proof

      let E be Field, R be Subring of E;

      now

        assume

         B: R is Field;

        the carrier of R c= the carrier of E & the addF of R = (the addF of E || the carrier of R) & the multF of R = (the multF of E || the carrier of R) & ( 1. R) = ( 1. E) & ( 0. R) = ( 0. E) by C0SP1:def 3;

        hence R is Subfield of E by EC_PF_1:def 1, B;

      end;

      hence thesis;

    end;

    registration

      let F be Field;

      let E be FieldExtension of F;

      cluster E -extending for FieldExtension of F;

      existence

      proof

        take E;

        E is Subring of E by LIOUVIL2: 18;

        hence thesis by FIELD_4:def 1;

      end;

    end

    notation

      let F be Field;

      let E be FieldExtension of F;

      antonym E is F -infinite for E is F -finite;

    end

    theorem :: FIELD_5:14

    

     sp: for F be Field, E be FieldExtension of F holds for K be E -extending FieldExtension of F holds ( VecSp (E,F)) is Subspace of ( VecSp (K,F))

    proof

      let F be Field, E be FieldExtension of F;

      let K be E -extending FieldExtension of F;

      set VK = ( VecSp (K,F)), VE = ( VecSp (E,F));

      

       H1: E is Subring of K by FIELD_4:def 1;

      then

       H2: the carrier of E c= the carrier of K by C0SP1:def 3;

      

       H3: the carrier of VE = the carrier of E & the carrier of VK = the carrier of K by FIELD_4:def 6;

      F is Subring of E by FIELD_4:def 1;

      then

       H4: the carrier of F c= the carrier of E by C0SP1:def 3;

      

       B1: the carrier of VE c= the carrier of VK by H1, H3, C0SP1:def 3;

      

       B2: ( 0. VE) = ( 0. E) by FIELD_4:def 6

      .= ( 0. K) by H1, C0SP1:def 3

      .= ( 0. VK) by FIELD_4:def 6;

      

       B3: the addF of VE = the addF of E by FIELD_4:def 6

      .= (the addF of K || the carrier of E) by H1, C0SP1:def 3

      .= (the addF of VK || the carrier of E) by FIELD_4:def 6

      .= (the addF of VK || the carrier of VE) by FIELD_4:def 6;

      

       B4: the lmult of VE = (the multF of E | [:the carrier of F, the carrier of VE:]) by H3, FIELD_4:def 6

      .= ((the multF of K || the carrier of E) | [:the carrier of F, the carrier of VE:]) by H1, C0SP1:def 3

      .= (the multF of K | [:the carrier of F, the carrier of VE:]) by H4, H3, ZFMISC_1: 96, RELAT_1: 74

      .= ((the multF of K | [:the carrier of F, the carrier of K:]) | [:the carrier of F, the carrier of VE:]) by H2, H3, ZFMISC_1: 96, RELAT_1: 74

      .= (the lmult of VK | [:the carrier of F, the carrier of VE:]) by FIELD_4:def 6;

      thus thesis by B1, B2, B3, B4, VECTSP_4:def 2;

    end;

    theorem :: FIELD_5:15

    for F be Field, E be FieldExtension of F holds for K be E -extending FieldExtension of F holds K is F -infinite or (E is F -finite & ( deg (E,F)) <= ( deg (K,F)))

    proof

      let F be Field, E be FieldExtension of F;

      let K be E -extending FieldExtension of F;

      set VK = ( VecSp (K,F)), VE = ( VecSp (E,F));

      now

        assume K is F -finite;

        then

        reconsider VK as finite-dimensional VectSp of F by FIELD_4:def 8;

        

         A: ( deg (K,F)) = ( dim VK) by FIELD_4:def 7;

        

         B: VE is Subspace of VK by sp;

        then

         C: ( dim VE) <= ( dim VK) by VECTSP_9: 25;

        thus E is F -finite by B, FIELD_4:def 8;

        thus ( deg (E,F)) <= ( deg (K,F)) by A, C, FIELD_4:def 7;

      end;

      hence thesis;

    end;

    theorem :: FIELD_5:16

    

     divmod: for F be Field, p be Polynomial of F holds for q be non zero Polynomial of F holds ( deg (p mod q)) < ( deg q)

    proof

      let F be Field, p be Polynomial of F;

      let q be non zero Polynomial of F;

      q <> ( 0_. F);

      then

      consider t be Polynomial of F such that

       C: p = (((p div q) *' q) + t) & ( deg t) < ( deg q) by HURWITZ:def 5;

      (p mod q) = ((((p div q) *' q) + t) - ((p div q) *' q)) by C, HURWITZ:def 6

      .= (t + (((p div q) *' q) - ((p div q) *' q))) by POLYNOM3: 26

      .= (t + ( 0_. F)) by POLYNOM3: 29;

      hence thesis by C;

    end;

    

     lempk: for F,K be Field st the carrier of F = the carrier of K & ( 0. F) = ( 0. K) holds the carrier of ( Polynom-Ring F) = the carrier of ( Polynom-Ring K)

    proof

      let F,K be Field;

      assume

       AS: the carrier of F = the carrier of K & ( 0. F) = ( 0. K);

       A:

      now

        let o be object;

        assume o in the carrier of ( Polynom-Ring F);

        then

        reconsider p = o as Polynomial of F by POLYNOM3:def 10;

        reconsider p1 = p as sequence of K by AS;

        for i be Nat st i >= ( len p) holds (p1 . i) = ( 0. K) by AS, ALGSEQ_1: 8;

        then p1 is finite-Support by ALGSEQ_1:def 1;

        hence o in the carrier of ( Polynom-Ring K) by POLYNOM3:def 10;

      end;

      now

        let o be object;

        assume o in the carrier of ( Polynom-Ring K);

        then

        reconsider p = o as Polynomial of K by POLYNOM3:def 10;

        reconsider p1 = p as sequence of F by AS;

        for i be Nat st i >= ( len p) holds (p1 . i) = ( 0. F) by AS, ALGSEQ_1: 8;

        then p1 is finite-Support by ALGSEQ_1:def 1;

        hence o in the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    begin

    definition

      let R be Ring;

      let p be Polynomial of R;

      :: FIELD_5:def1

      attr p is linear means

      : defl: ( deg p) = 1;

    end

    registration

      let R be non degenerated Ring;

      cluster linear for Polynomial of R;

      existence

      proof

        take ( rpoly (1,( 0. R)));

        thus thesis by HURWITZ: 27;

      end;

      cluster non linear for Polynomial of R;

      existence

      proof

        take ( 0_. R);

        thus thesis by HURWITZ: 20;

      end;

      cluster linear for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        reconsider o = ( rpoly (1,( 1. R))) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

        take o;

        thus thesis by HURWITZ: 27;

      end;

      cluster non linear for Element of the carrier of ( Polynom-Ring R);

      existence

      proof

        reconsider o = ( 0_. R) as Element of the carrier of ( Polynom-Ring R) by POLYNOM3:def 10;

        take o;

        thus thesis by HURWITZ: 20;

      end;

    end

    registration

      let R be non degenerated Ring;

      cluster zero -> non linear for Polynomial of R;

      coherence

      proof

        let p be Polynomial of R;

        assume p is zero;

        then p = ( 0_. R) by UPROOTS:def 5;

        hence thesis by HURWITZ: 20;

      end;

      cluster constant -> non linear for Polynomial of R;

      coherence by RATFUNC1:def 2;

    end

    registration

      let F be Field;

      cluster linear -> with_roots for Polynomial of F;

      coherence

      proof

        let p be Polynomial of F;

        assume p is linear;

        then

        consider x,z be Element of F such that

         A: x <> ( 0. F) & p = (x * ( rpoly (1,z))) by HURWITZ: 28;

        thus p is with_roots by A;

      end;

    end

    registration

      let F be Field;

      cluster linear -> irreducible for Element of the carrier of ( Polynom-Ring F);

      coherence by RING_4: 44;

    end

    registration

      let F be Field;

      cluster non linear with_roots -> reducible for Element of the carrier of ( Polynom-Ring F);

      coherence

      proof

        let p be Element of the carrier of ( Polynom-Ring F);

        assume

         AS: p is non linear with_roots;

        then

        consider a be Element of F such that

         A: a is_a_root_of p by POLYNOM5:def 8;

        consider q1 be Polynomial of F such that

         B: p = (( rpoly (1,a)) *' q1) by A, HURWITZ: 33;

        reconsider q = q1 as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        

         C: q divides p by B, RING_4: 1;

        per cases ;

          suppose p = ( 0_. F);

          hence thesis;

        end;

          suppose

           L: p <> ( 0_. F);

          then

           M: q1 <> ( 0_. F) by B;

          

          then

           D: ( deg p) = (( deg ( rpoly (1,a))) + ( deg q1)) by B, HURWITZ: 23

          .= (1 + ( deg q1)) by HURWITZ: 27;

          reconsider degp = ( deg p), degq = ( deg q) as Element of NAT by M, L, FIELD_1: 1;

          (1 + degq) >= (1 + 1) by D, AS, NAT_1: 23;

          then 1 <= degq by XREAL_1: 6;

          hence thesis by C, D, NAT_1: 19, RING_4: 40;

        end;

      end;

    end

    registration

      let R be domRing;

      let p be linear Polynomial of R;

      let q be non constant Polynomial of R;

      cluster (p *' q) -> non linear;

      coherence

      proof

        reconsider p1 = p, q1 = q as Polynomial of R;

        q <> ( 0_. R) & p <> ( 0_. R);

        then

         B: ( deg (p1 *' q1)) = (( deg p) + ( deg q)) by HURWITZ: 23;

        ( deg p) = 1 by defl;

        hence (p *' q) is non linear by RATFUNC1:def 2, B;

      end;

    end

    registration

      let F be Field;

      let p be linear Polynomial of F;

      let q be non constant Polynomial of F;

      cluster (p *' q) -> with_roots;

      coherence ;

    end

    begin

    

     lemdis: for F be polynomial_disjoint Field holds for p be non constant Element of the carrier of ( Polynom-Ring F) holds (F,( Polynom-Ring p)) are_disjoint

    proof

      let F be polynomial_disjoint Field, p be non constant Element of the carrier of ( Polynom-Ring F);

      now

        assume not (F,( Polynom-Ring p)) are_disjoint ;

        then

         A: (( [#] F) /\ ( [#] ( Polynom-Ring p))) <> {} by FIELD_2:def 1;

        let a be Element of (the carrier of F /\ the carrier of ( Polynom-Ring p));

        

         B: a in the carrier of F & a in the carrier of ( Polynom-Ring p) by A, XBOOLE_0:def 4;

        the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

        then

        consider q be Polynomial of F such that

         C: a = q & ( deg q) < ( deg p) by B;

        a in the carrier of ( Polynom-Ring F) by C, POLYNOM3:def 10;

        then a in (( [#] F) /\ ( [#] ( Polynom-Ring F))) by B, XBOOLE_0:def 4;

        hence contradiction by FIELD_3:def 3;

      end;

      hence thesis;

    end;

    definition

      let F be Field, p be non constant Element of the carrier of ( Polynom-Ring F);

      :: FIELD_5:def2

      func canHomP p -> Function of F, ( Polynom-Ring p) means

      : defch: for a be Element of F holds (it . a) = (a | F);

      existence

      proof

        set R = F, B = ( Polynom-Ring p);

        defpred P[ object, object] means ex a be Element of R st $1 = a & $2 = (a | R);

        

         X: for x be object st x in the carrier of R holds ex y be object st y in the carrier of B & P[x, y]

        proof

          let x be object;

          assume x in the carrier of R;

          then

          reconsider a = x as Element of R;

           not ( deg p) <= 0 & ( deg (a | R)) <= 0 by RING_4:def 4, RATFUNC1:def 2;

          then (a | F) in { q where q be Polynomial of F : ( deg q) < ( deg p) };

          then

          reconsider y = (a | R) as Element of B by RING_4:def 8;

          take y;

          thus thesis;

        end;

        consider g be Function of the carrier of R, the carrier of B such that

         Z: for x be object st x in the carrier of R holds P[x, (g . x)] from FUNCT_2:sch 1( X);

        now

          let x be Element of R;

          consider a be Element of R such that

           H: x = a & (g . x) = (a | R) by Z;

          thus (g . x) = (x | R) by H;

        end;

        then

        consider f be Function of R, B such that

         Y: for x be Element of R holds (f . x) = (x | R);

        take f;

        thus thesis by Y;

      end;

      uniqueness

      proof

        set R = F, B = ( Polynom-Ring p);

        let g1,g2 be Function of R, B such that

         A1: for a be Element of R holds (g1 . a) = (a | R) and

         A2: for a be Element of R holds (g2 . a) = (a | R);

        

         A: ( dom g1) = the carrier of R by FUNCT_2:def 1

        .= ( dom g2) by FUNCT_2:def 1;

        now

          let x be object;

          assume x in ( dom g1);

          then

          reconsider a = x as Element of R;

          

          thus (g1 . x) = (a | R) by A1

          .= (g2 . x) by A2;

        end;

        hence thesis by A;

      end;

    end

    registration

      let F be Field, p be non constant Element of the carrier of ( Polynom-Ring F);

      cluster ( canHomP p) -> additive multiplicative unity-preserving one-to-one;

      coherence

      proof

        set R = F, RX = ( Polynom-Ring F), f = ( canHomP p), B = ( Polynom-Ring p);

        hereby

          let x,y be Element of R;

          

           B: (f . x) = (x | R) & (f . y) = (y | R) by defch;

          

           A: [(f . x), (f . y)] in [:the carrier of B, the carrier of B:] by ZFMISC_1:def 2;

          reconsider fx = (f . x), fy = (f . y) as Element of the carrier of RX by B, POLYNOM3:def 10;

          

          thus ((f . x) + (f . y)) = ((the addF of RX || the carrier of B) . ((f . x),(f . y))) by RING_4:def 8

          .= (fx + fy) by A, FUNCT_1: 49

          .= ((x | R) + (y | R)) by B, POLYNOM3:def 10

          .= ((x + y) | R) by RING_4: 17

          .= (f . (x + y)) by defch;

        end;

        hereby

          let x,y be Element of R;

          

           B: (f . x) = (x | R) & (f . y) = (y | R) by defch;

          

           A: [(f . x), (f . y)] in [:the carrier of B, the carrier of B:] by ZFMISC_1:def 2;

          reconsider fx = (f . x), fy = (f . y) as Element of the carrier of RX by B, POLYNOM3:def 10;

          reconsider p1 = p as Polynomial of F;

          

           C: ( deg ((x * y) | R)) <= 0 & ( deg p) > 0 by RING_4:def 4, RATFUNC1:def 2;

          

          thus ((f . x) * (f . y)) = ((( poly_mult_mod p) || the carrier of B) . ((f . x),(f . y))) by RING_4:def 8

          .= (( poly_mult_mod p) . (fx,fy)) by A, FUNCT_1: 49

          .= (((x | R) *' (y | R)) mod p) by B, RING_4:def 7

          .= (((x * y) | R) mod p) by RING_4: 18

          .= ((x * y) | R) by C, RING_4: 2

          .= (f . (x * y)) by defch;

        end;

        

        thus (f . ( 1_ R)) = (( 1. R) | R) by defch

        .= ( 1_. R) by RING_4: 14

        .= ( 1_ ( Polynom-Ring p)) by RING_4:def 8;

        now

          let x1,x2 be object;

          assume

           AS: x1 in the carrier of R & x2 in the carrier of R & (f . x1) = (f . x2);

          then

          reconsider a = x1, b = x2 as Element of R;

          (a | R) = (f . x2) by AS, defch

          .= (b | R) by defch;

          hence x1 = x2 by RING_4: 19;

        end;

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

      end;

    end

    registration

      let F be Field;

      let p be non constant Element of the carrier of ( Polynom-Ring F);

      cluster ( Polynom-Ring p) -> F -homomorphicF -monomorphic;

      coherence

      proof

        ( canHomP p) is monomorphism;

        hence thesis by RING_3:def 3;

      end;

    end

    registration

      let F be polynomial_disjoint Field;

      let p be irreducible Element of the carrier of ( Polynom-Ring F);

      cluster ( embField ( canHomP p)) -> add-associative right_complementable associative distributive almost_left_invertible;

      coherence by lemdis, FIELD_2: 12;

    end

    registration

      let F be polynomial_disjoint Field;

      let p be irreducible Element of the carrier of ( Polynom-Ring F);

      cluster ( embField ( canHomP p)) -> F -extending;

      coherence

      proof

        F is Subfield of ( embField ( canHomP p)) by FIELD_2: 17;

        then F is Subring of ( embField ( canHomP p)) by pr1;

        hence thesis by FIELD_4:def 1;

      end;

    end

    definition

      let F be polynomial_disjoint Field;

      let p be irreducible Element of the carrier of ( Polynom-Ring F);

      :: FIELD_5:def3

      func KrRootP p -> Element of ( embField ( canHomP p)) equals (((( emb_iso ( canHomP p)) " ) * (( KroneckerIso p) " )) . ( KrRoot p));

      coherence

      proof

        set K = ( KroneckerField (F,p));

        

         E9: ( emb_iso ( canHomP p)) is onto by lemdis, FIELD_2: 15;

        ( rng ( KroneckerIso p)) = the carrier of K by FUNCT_2:def 3;

        then ( KrRoot p) in ( rng ( KroneckerIso p));

        then

         E3: ( KrRoot p) in ( dom (( KroneckerIso p) " )) by FUNCT_1: 32;

        then

         E6: ((( KroneckerIso p) " ) . ( KrRoot p)) in ( rng (( KroneckerIso p) " )) by FUNCT_1:def 3;

        

         E10: ((( KroneckerIso p) " ) . ( KrRoot p)) in ( dom ( KroneckerIso p)) by E6, FUNCT_1: 33;

        ( dom (( emb_iso ( canHomP p)) " )) = the carrier of ( Polynom-Ring p) by E9, FUNCT_1: 33

        .= ( dom ( KroneckerIso p)) by FUNCT_2:def 1;

        then ((( emb_iso ( canHomP p)) " ) . ((( KroneckerIso p) " ) . ( KrRoot p))) in ( rng (( emb_iso ( canHomP p)) " )) by E10, FUNCT_1: 3;

        then ((( emb_iso ( canHomP p)) " ) . ((( KroneckerIso p) " ) . ( KrRoot p))) in ( dom ( emb_iso ( canHomP p))) by FUNCT_1: 33;

        hence thesis by E3, FUNCT_1: 13;

      end;

    end

    theorem :: FIELD_5:17

    for F be polynomial_disjoint Field holds for p be irreducible Element of the carrier of ( Polynom-Ring F) holds ( Ext_eval (p,( KrRootP p))) = ( 0. F)

    proof

      let F be polynomial_disjoint Field;

      let p be irreducible Element of the carrier of ( Polynom-Ring F);

      set K = ( KroneckerField (F,p)), u = ( KrRoot p), E = ( embField ( canHomP p));

      set h = (( KroneckerIso p) * ( emb_iso ( canHomP p)));

      reconsider h as Function of E, K by FUNCT_2: 13;

      ( emb_iso ( canHomP p)) is onto by lemdis, FIELD_2: 15;

      then

       B: h is one-to-one onto by FUNCT_2: 27;

      ( emb_iso ( canHomP p)) is additive multiplicative by lemdis, FIELD_2: 13, FIELD_2: 14;

      then

       C: h is linear by RINGCAT1: 1;

      then

      reconsider P = K as E -isomorphic Field by B, RING_3:def 4;

      reconsider iso = h as Isomorphism of E, P by B, C;

      reconsider E as P -isomorphic Field by RING_3: 74;

      reconsider E as P -homomorphic Field;

      reconsider isoi = (iso " ) as Homomorphism of P, E by RING_3: 73;

      reconsider t = ( emb (p,p)) as Element of the carrier of ( Polynom-Ring P);

      reconsider ui = u as Element of P;

      u is_a_root_of ( emb (p,p)) by FIELD_1: 42;

      then

       X: ( eval ((( PolyHom isoi) . t),(isoi . ui))) = ( 0. E) by FIELD_1: 34, POLYNOM5:def 7;

      

       Y: (( PolyHom isoi) . t) = p

      proof

        set g = (( PolyHom isoi) . t);

        

         A: for a be Element of F holds (isoi . (( emb p) . a)) = a

        proof

          let a be Element of F;

          reconsider b = (a | F) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          

           A12: the carrier of ( Polynom-Ring p) = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

          ( deg (a | F)) <= 0 & ( deg p) > 0 by RATFUNC1:def 2, RING_4:def 4;

          then

           A3: (a | F) in the carrier of ( Polynom-Ring p) by A12;

          then

          reconsider b1 = (a | F) as Element of ( Polynom-Ring p);

          reconsider v = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b)) as Element of ( KroneckerField (F,p)) by RING_1: 12;

          

           A5: b1 in ( dom ( KroneckerIso p)) by A3, FUNCT_2:def 1;

          

           A7: ( dom (( KroneckerIso p) " )) = ( rng ( KroneckerIso p)) by FUNCT_1: 33

          .= the carrier of K by FUNCT_2:def 3;

          (( KroneckerIso p) . b1) = v by FIELD_4:def 9;

          then

           A6: ((( KroneckerIso p) " ) . v) = b1 by A5, FUNCT_1: 34;

          F is Subfield of ( embField ( canHomP p)) by FIELD_2: 17;

          then the carrier of F c= the carrier of ( embField ( canHomP p)) by EC_PF_1:def 1;

          then

          reconsider aa = a as Element of ( embField ( canHomP p));

          

           A9: ( dom ( emb_iso ( canHomP p))) = the carrier of E by FUNCT_2:def 1;

          aa in F;

          

          then (( emb_iso ( canHomP p)) . aa) = (( canHomP p) . aa) by FIELD_2:def 8

          .= (a | F) by defch;

          then

           A2: ((( emb_iso ( canHomP p)) " ) . b1) = aa by A9, FUNCT_1: 34;

          

          thus (isoi . (( emb p) . a)) = (isoi . v) by FIELD_1: 39

          .= (((( emb_iso ( canHomP p)) " ) * (( KroneckerIso p) " )) . v) by FUNCT_1: 44

          .= a by A2, A6, A7, FUNCT_1: 13;

        end;

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Element of NAT ;

          (g . i) = (isoi . (( emb (p,p)) . i)) by FIELD_1:def 2

          .= (isoi . ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),((p . i) | F)))) by FIELD_1: 40

          .= (isoi . (( emb p) . (p . i))) by FIELD_1: 39;

          hence (g . x) = (p . x) by A;

        end;

        hence thesis;

      end;

      

       F0: ( dom ( KroneckerIso p)) = the carrier of ( Polynom-Ring p) by FUNCT_2:def 1;

      

       E5: ( rng ( KroneckerIso p)) = the carrier of K by FUNCT_2:def 3;

      then ( KrRoot p) in ( rng ( KroneckerIso p));

      then

       E3: ( KrRoot p) in ( dom (( KroneckerIso p) " )) by FUNCT_1: 32;

      then

       E6: ((( KroneckerIso p) " ) . ( KrRoot p)) in ( rng (( KroneckerIso p) " )) by FUNCT_1:def 3;

      

       E9: ( emb_iso ( canHomP p)) is onto by lemdis, FIELD_2: 15;

      then

       E4: ((( KroneckerIso p) " ) . ( KrRoot p)) in ( rng ( emb_iso ( canHomP p))) by E6, F0, FUNCT_1: 33;

      

       E10: ((( KroneckerIso p) " ) . ( KrRoot p)) in ( dom ( KroneckerIso p)) by E6, FUNCT_1: 33;

      ( dom (( emb_iso ( canHomP p)) " )) = the carrier of ( Polynom-Ring p) by E9, FUNCT_1: 33

      .= ( dom ( KroneckerIso p)) by FUNCT_2:def 1;

      then ((( emb_iso ( canHomP p)) " ) . ((( KroneckerIso p) " ) . ( KrRoot p))) in ( rng (( emb_iso ( canHomP p)) " )) by E10, FUNCT_1: 3;

      then ((( emb_iso ( canHomP p)) " ) . ((( KroneckerIso p) " ) . ( KrRoot p))) in ( dom ( emb_iso ( canHomP p))) by FUNCT_1: 33;

      then

       E2: (((( emb_iso ( canHomP p)) " ) * (( KroneckerIso p) " )) . ( KrRoot p)) in ( dom ( emb_iso ( canHomP p))) by E3, FUNCT_1: 13;

      (iso . ( KrRootP p)) = (( KroneckerIso p) . (( emb_iso ( canHomP p)) . (((( emb_iso ( canHomP p)) " ) * (( KroneckerIso p) " )) . ( KrRoot p)))) by E2, FUNCT_1: 13

      .= (( KroneckerIso p) . (( emb_iso ( canHomP p)) . ((( emb_iso ( canHomP p)) " ) . ((( KroneckerIso p) " ) . ( KrRoot p))))) by E3, FUNCT_1: 13

      .= (( KroneckerIso p) . ((( KroneckerIso p) " ) . ( KrRoot p))) by E4, FUNCT_1: 35

      .= ( KrRoot p) by E5, FUNCT_1: 35;

      then (isoi . ui) = ( KrRootP p) by FUNCT_2: 26;

      

      hence ( Ext_eval (p,( KrRootP p))) = ( 0. E) by X, Y, FIELD_4: 26

      .= ( 0. F) by FIELD_2:def 7;

    end;

    begin

    theorem :: FIELD_5:18

    

     polyd: for F be Field holds for p be linear Element of the carrier of ( Polynom-Ring F) holds (( Polynom-Ring p),F) are_isomorphic & the carrier of ( embField ( canHomP p)) = the carrier of F

    proof

      let F be Field;

      let p be linear Element of the carrier of ( Polynom-Ring F);

      set FP = ( Polynom-Ring p), f = ( canHomP p);

      

       H: the carrier of FP = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

       A:

      now

        let o be object;

        assume o in the carrier of FP;

        then

        consider q be Polynomial of F such that

         B: q = o & ( deg q) < ( deg p) by H;

        reconsider q as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

        ( deg q) < 1 by B, defl;

        then (( deg q) + 1) <= 1 by INT_1: 7;

        then ((( deg q) + 1) - 1) <= (1 - 1) by XREAL_1: 9;

        then

        consider a be Element of F such that

         C: q = (a | F) by RING_4: 20, RING_4:def 4;

        

         D: (f . a) = o by B, C, defch;

        ( dom f) = the carrier of F by FUNCT_2:def 1;

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

      end;

       X:

      now

        let o be object;

        assume

         B: o in ( rng f);

        ( rng f) c= the carrier of FP by RELAT_1:def 19;

        hence o in the carrier of FP by B;

      end;

      then

       B: ( rng f) = the carrier of FP by A, TARSKI: 2;

      f is monomorphism onto by X, A, TARSKI: 2;

      then (F,( Polynom-Ring p)) are_isomorphic ;

      hence (( Polynom-Ring p),F) are_isomorphic ;

      

       X: ( [#] FP) = the carrier of FP & ( [#] F) = the carrier of F;

      

      thus the carrier of ( embField ( canHomP p)) = ( carr f) by FIELD_2:def 7

      .= ((the carrier of FP \ ( rng f)) \/ the carrier of F) by X, FIELD_2:def 2

      .= ( {} \/ the carrier of F) by B, XBOOLE_1: 37

      .= the carrier of F;

    end;

    theorem :: FIELD_5:19

    for F be strict Field holds for p be linear Element of the carrier of ( Polynom-Ring F) holds ( embField ( canHomP p)) = F

    proof

      let F be strict Field;

      let p be linear Element of the carrier of ( Polynom-Ring F);

      set FP = ( embField ( canHomP p)), f = ( canHomP p);

      

       X: ( [#] F) = the carrier of F & ( [#] ( Polynom-Ring p)) = the carrier of ( Polynom-Ring p);

      

       H: the carrier of F = the carrier of ( embField f) by polyd;

      

       A: ( 1. FP) = ( 1. F) & ( 0. FP) = ( 0. F) by FIELD_2:def 7;

      

       B: ( dom the addF of FP) = [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1

      .= ( dom the addF of F) by H, FUNCT_2:def 1;

      now

        let x be Element of ( dom the addF of F);

        consider o be Element of [:the carrier of F, the carrier of F:] such that

         B1: x = o;

        consider a,b be object such that

         B2: a in the carrier of F & b in the carrier of F & o = [a, b] by ZFMISC_1:def 2;

        a in ((the carrier of ( Polynom-Ring p) \ ( rng f)) \/ the carrier of F) & b in ((the carrier of ( Polynom-Ring p) \ ( rng f)) \/ the carrier of F) by B2, XBOOLE_0:def 3;

        then

        reconsider a, b as Element of ( carr f) by X, FIELD_2:def 2;

        

        thus (the addF of FP . x) = (( addemb f) . (a,b)) by B1, B2, FIELD_2:def 7

        .= ( addemb (f,a,b)) by FIELD_2:def 4

        .= (the addF of F . (a,b)) by B2, X, FIELD_2:def 3

        .= (the addF of F . x) by B1, B2;

      end;

      then

       C: the addF of FP = the addF of F by B;

      

       B: ( dom the multF of FP) = [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1

      .= ( dom the multF of F) by H, FUNCT_2:def 1;

      now

        let x be Element of ( dom the multF of F);

        consider o be Element of [:the carrier of F, the carrier of F:] such that

         B1: x = o;

        consider a,b be object such that

         B2: a in the carrier of F & b in the carrier of F & o = [a, b] by ZFMISC_1:def 2;

        a in ((the carrier of ( Polynom-Ring p) \ ( rng f)) \/ the carrier of F) & b in ((the carrier of ( Polynom-Ring p) \ ( rng f)) \/ the carrier of F) by B2, XBOOLE_0:def 3;

        then

        reconsider a, b as Element of ( carr f) by X, FIELD_2:def 2;

        

        thus (the multF of FP . x) = (( multemb f) . (a,b)) by B1, B2, FIELD_2:def 7

        .= ( multemb (f,a,b)) by FIELD_2:def 6

        .= (the multF of F . (a,b)) by B2, X, FIELD_2:def 5

        .= (the multF of F . x) by B1, B2;

      end;

      then the multF of FP = the multF of F by B;

      hence thesis by A, C, polyd;

    end;

    theorem :: FIELD_5:20

    

     polyd1: for F be Field holds for p be linear Element of the carrier of ( Polynom-Ring F) holds ((( Polynom-Ring F) / ( {p} -Ideal )),F) are_isomorphic & the carrier of ( embField ( emb p)) = the carrier of F

    proof

      let F be Field;

      let p be linear Element of the carrier of ( Polynom-Ring F);

      set FP = (( Polynom-Ring F) / ( {p} -Ideal )), I = ( {p} -Ideal ), f = ( emb p), FX = ( Polynom-Ring F);

      

       A: (FP,( Polynom-Ring p)) are_isomorphic by RING_4: 48;

      (( Polynom-Ring p),F) are_isomorphic by polyd;

      hence ((( Polynom-Ring F) / ( {p} -Ideal )),F) are_isomorphic by A, RING_3: 44;

       B:

      now

        let q be Element of the carrier of FX;

        

         B1: q = (((q div p) *' p) + (q mod p)) by RING_4: 4;

        reconsider r = (q mod p), d = (q div p) as Element of the carrier of FX by POLYNOM3:def 10;

        ( deg r) < ( deg p) by divmod;

        then ( deg r) < 1 by defl;

        then (( deg r) + 1) <= 1 by INT_1: 7;

        then ((( deg r) + 1) - 1) <= (1 - 1) by XREAL_1: 9;

        then

        reconsider r as constant Element of the carrier of FX by RING_4:def 4;

        ((q div p) *' p) = (d * p) by POLYNOM3:def 10;

        then q = ((d * p) + r) by B1, POLYNOM3:def 10;

        

        then

         B2: (q - r) = ((d * p) + (r - r)) by RLVECT_1: 28

        .= ((d * p) + ( 0. FX)) by RLVECT_1: 15;

        ( {p} -Ideal ) = the set of all (p * c) where c be Element of FX by IDEAL_1: 64;

        then (p * d) in I;

        then (d * p) in I by GROUP_1:def 12;

        then ( Class (( EqRel (FX,I)),q)) = ( Class (( EqRel (FX,I)),r)) by B2, RING_1: 6;

        hence ex r be constant Element of the carrier of FX st ( Class (( EqRel (FX,I)),q)) = ( Class (( EqRel (FX,I)),r));

      end;

       E:

      now

        let o be object;

        assume o in the carrier of FP;

        then

        consider q be Element of the carrier of FX such that

         E1: o = ( Class (( EqRel (FX,I)),q)) by RING_1: 11;

        consider r be constant Element of the carrier of FX such that

         E2: ( Class (( EqRel (FX,I)),q)) = ( Class (( EqRel (FX,I)),r)) by B;

        consider a be Element of F such that

         E3: (a | F) = r by RING_4: 20;

        

         E4: (f . a) = o by E1, E2, E3, FIELD_1: 39;

        ( dom f) = the carrier of F by FUNCT_2:def 1;

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

      end;

      now

        let o be object;

        assume

         B: o in ( rng f);

        ( rng f) c= the carrier of FP by RELAT_1:def 19;

        hence o in the carrier of FP by B;

      end;

      then

       C: ( rng f) = the carrier of FP by E, TARSKI: 2;

      

       X: ( [#] F) = the carrier of F & ( [#] FP) = the carrier of FP;

      

      thus the carrier of ( embField ( emb p)) = ( carr f) by FIELD_2:def 7

      .= ((the carrier of FP \ ( rng f)) \/ the carrier of F) by X, FIELD_2:def 2

      .= ( {} \/ the carrier of F) by C, XBOOLE_1: 37

      .= the carrier of F;

    end;

    theorem :: FIELD_5:21

    for F be strict Field holds for p be linear Element of the carrier of ( Polynom-Ring F) holds ( embField ( emb p)) = F

    proof

      let F be strict Field;

      let p be linear Element of the carrier of ( Polynom-Ring F);

      set FP = ( embField ( emb p)), f = ( emb p), K = (( Polynom-Ring F) / ( {p} -Ideal ));

      

       X: ( [#] K) = the carrier of K & ( [#] F) = the carrier of F;

      

       H: the carrier of F = the carrier of ( embField f) by polyd1;

      

       A: ( 1. FP) = ( 1. F) & ( 0. FP) = ( 0. F) by FIELD_2:def 7;

      

       B: ( dom the addF of FP) = [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1

      .= ( dom the addF of F) by H, FUNCT_2:def 1;

      now

        let x be Element of ( dom the addF of F);

        consider o be Element of [:the carrier of F, the carrier of F:] such that

         B1: x = o;

        consider a,b be object such that

         B2: a in the carrier of F & b in the carrier of F & o = [a, b] by ZFMISC_1:def 2;

        a in ((the carrier of K \ ( rng f)) \/ the carrier of F) & b in ((the carrier of K \ ( rng f)) \/ the carrier of F) by B2, XBOOLE_0:def 3;

        then

        reconsider a, b as Element of ( carr f) by X, FIELD_2:def 2;

        

        thus (the addF of FP . x) = (( addemb f) . (a,b)) by B1, B2, FIELD_2:def 7

        .= ( addemb (f,a,b)) by FIELD_2:def 4

        .= (the addF of F . (a,b)) by B2, X, FIELD_2:def 3

        .= (the addF of F . x) by B1, B2;

      end;

      then

       C: the addF of FP = the addF of F by B;

      

       B: ( dom the multF of FP) = [:the carrier of FP, the carrier of FP:] by FUNCT_2:def 1

      .= ( dom the multF of F) by H, FUNCT_2:def 1;

      now

        let x be Element of ( dom the multF of F);

        consider o be Element of [:the carrier of F, the carrier of F:] such that

         B1: x = o;

        consider a,b be object such that

         B2: a in the carrier of F & b in the carrier of F & o = [a, b] by ZFMISC_1:def 2;

        a in ((the carrier of K \ ( rng f)) \/ the carrier of F) & b in ((the carrier of K \ ( rng f)) \/ the carrier of F) by B2, XBOOLE_0:def 3;

        then

        reconsider a, b as Element of ( carr f) by X, FIELD_2:def 2;

        

        thus (the multF of FP . x) = (( multemb f) . (a,b)) by B1, B2, FIELD_2:def 7

        .= ( multemb (f,a,b)) by FIELD_2:def 6

        .= (the multF of F . (a,b)) by B2, X, FIELD_2:def 5

        .= (the multF of F . x) by B1, B2;

      end;

      then the multF of FP = the multF of F by B;

      hence thesis by A, C, polyd1;

    end;

    theorem :: FIELD_5:22

    for F be polynomial_disjoint Field, p be irreducible Element of the carrier of ( Polynom-Ring F) holds ( embField ( canHomP p)) is polynomial_disjoint iff p is linear

    proof

      let F be polynomial_disjoint Field, p be irreducible Element of the carrier of ( Polynom-Ring F);

      set FP = ( Polynom-Ring p), K = ( embField ( canHomP p)), X = <%( 0. F), ( 1. F)%>;

      

       X: ( [#] F) = the carrier of F & ( [#] ( Polynom-Ring p)) = the carrier of ( Polynom-Ring p);

       A:

      now

        assume

         AS: ( deg p) > 1;

        

         H: the carrier of FP = { q where q be Polynomial of F : ( deg q) < ( deg p) } by RING_4:def 8;

        ( len X) = 2 by POLYNOM5: 40;

        then

         D: ( deg X) = (2 - 1) by HURWITZ:def 2;

        then

         C: X in the carrier of FP by H, AS;

        now

          assume X in ( rng ( canHomP p));

          then

          consider o be object such that

           B1: o in ( dom ( canHomP p)) & (( canHomP p) . o) = X by FUNCT_1:def 3;

          reconsider a = o as Element of F by B1;

          X = (a | F) by B1, defch;

          hence contradiction by D, RATFUNC1:def 2;

        end;

        then X in (the carrier of FP \ ( rng ( canHomP p))) by C, XBOOLE_0:def 5;

        then X in ((the carrier of FP \ ( rng ( canHomP p))) \/ the carrier of F) by XBOOLE_0:def 3;

        then X in ( carr ( canHomP p)) by X, FIELD_2:def 2;

        then

         A: X in the carrier of K by FIELD_2:def 7;

        now

          let n be Element of NAT ;

          per cases by NAT_1: 23;

            suppose

             B: n = 0 ;

            

            hence ( <%( 0. F), ( 1. F)%> . n) = ( 0. F) by POLYNOM5: 38

            .= ( 0. K) by FIELD_2:def 7

            .= ( <%( 0. K), ( 1. K)%> . n) by B, POLYNOM5: 38;

          end;

            suppose

             B: n = 1;

            

            hence ( <%( 0. F), ( 1. F)%> . n) = ( 1. F) by POLYNOM5: 38

            .= ( 1. K) by FIELD_2:def 7

            .= ( <%( 0. K), ( 1. K)%> . n) by B, POLYNOM5: 38;

          end;

            suppose

             B: n >= 2;

            

            hence ( <%( 0. F), ( 1. F)%> . n) = ( 0. F) by POLYNOM5: 38

            .= ( 0. K) by FIELD_2:def 7

            .= ( <%( 0. K), ( 1. K)%> . n) by B, POLYNOM5: 38;

          end;

        end;

        then <%( 0. F), ( 1. F)%> = <%( 0. K), ( 1. K)%>;

        then X in the carrier of ( Polynom-Ring K) by POLYNOM3:def 10;

        then X in (( [#] K) /\ ( [#] ( Polynom-Ring K))) by A, XBOOLE_0:def 4;

        hence K is non polynomial_disjoint by FIELD_3:def 3;

      end;

      

       H: ( 0. K) = ( 0. F) by FIELD_2:def 7;

       B:

      now

        assume

         C: p is linear;

        then

         D: ( [#] ( Polynom-Ring K)) = ( [#] ( Polynom-Ring F)) by H, lempk, polyd;

        ( [#] K) = ( [#] F) by C, polyd;

        then (( [#] K) /\ ( [#] ( Polynom-Ring K))) = {} by D, FIELD_3:def 3;

        hence K is polynomial_disjoint by FIELD_3:def 3;

      end;

      now

        assume

         C: K is polynomial_disjoint;

        ( deg p) >= ( 0 + 1) by INT_1: 7, RING_4:def 4;

        hence p is linear by A, C, XXREAL_0: 1;

      end;

      hence thesis by B;

    end;

    theorem :: FIELD_5:23

    for F be Field, p be irreducible Element of the carrier of ( Polynom-Ring F) holds for E be polynomial_disjoint Field st E = ( embField ( emb p)) holds F is polynomial_disjoint

    proof

      let F be Field, p be irreducible Element of the carrier of ( Polynom-Ring F);

      let E be polynomial_disjoint Field;

      assume

       AS1: E = ( embField ( emb p));

      assume

       AS2: F is non polynomial_disjoint;

      

       H: F is Subfield of E by AS1, FIELD_2: 17;

      then

      reconsider K = E as FieldExtension of F by FIELD_4: 7;

      

       A: the carrier of F c= the carrier of K by H, EC_PF_1:def 1;

      set o = the Element of (the carrier of F /\ the carrier of ( Polynom-Ring F));

      (( [#] F) /\ ( [#] ( Polynom-Ring F))) <> {} by AS2, FIELD_3:def 3;

      then

       B: o in the carrier of F & o in the carrier of ( Polynom-Ring F) by XBOOLE_0:def 4;

      the carrier of ( Polynom-Ring F) c= the carrier of ( Polynom-Ring K) by FIELD_4: 10;

      then o in (( [#] K) /\ ( [#] ( Polynom-Ring K))) by A, B, XBOOLE_0:def 4;

      hence thesis by FIELD_3:def 3;

    end;

    

     Disj1: for n be non trivial Nat holds for p be Element of the carrier of ( Polynom-Ring ( Z/ n)) holds (the carrier of ( Z/ n) /\ the carrier of (( Polynom-Ring ( Z/ n)) / ( {p} -Ideal ))) = {}

    proof

      let n be non trivial Nat;

      let p be Element of the carrier of ( Polynom-Ring ( Z/ n));

      set F = ( Z/ n);

      set FX = ( Polynom-Ring F), I = ( {p} -Ideal );

      set K = (( Polynom-Ring F) / ( {p} -Ideal ));

      set x = the Element of (the carrier of F /\ the carrier of K);

      now

        assume

         AS: (the carrier of F /\ the carrier of K) <> {} ;

        reconsider x as Element of F by AS, XBOOLE_0:def 4;

        reconsider q = x as Element of K by AS, XBOOLE_0:def 4;

        consider a be Element of FX such that

         A1: q = ( Class (( EqRel (FX,I)),a)) by RING_1: 11;

        reconsider pa = a as Polynomial of F by POLYNOM3:def 10;

        (a - a) = ( 0. FX) by RLVECT_1: 15;

        then

         A2: a in q by A1, RING_1: 5, IDEAL_1: 3;

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

        then x in ( Segm n);

        then

        reconsider k = x as Element of omega ;

        k = { m where m be Nat : m < k } by AXIOMS: 4;

        then

        consider m be Nat such that

         B1: a = m & m < k by A2;

        ( dom pa) = NAT by FUNCT_2:def 1;

        hence contradiction by B1;

      end;

      hence thesis;

    end;

    

     Disj2: for p be Element of the carrier of ( Polynom-Ring F_Rat ) holds (the carrier of F_Rat /\ the carrier of (( Polynom-Ring F_Rat ) / ( {p} -Ideal ))) = {}

    proof

      let p be Element of the carrier of ( Polynom-Ring F_Rat );

      set F = F_Rat ;

      set FX = ( Polynom-Ring F), I = ( {p} -Ideal );

      set K = (( Polynom-Ring F) / ( {p} -Ideal ));

      set x = the Element of (the carrier of F /\ the carrier of K);

      now

        assume

         AS: (the carrier of F /\ the carrier of K) <> {} ;

        reconsider x as Element of F by AS, XBOOLE_0:def 4;

        reconsider q = x as Element of K by AS, XBOOLE_0:def 4;

        consider a be Element of FX such that

         A1: q = ( Class (( EqRel (FX,I)),a)) by RING_1: 11;

        reconsider pa = a as Polynomial of F by POLYNOM3:def 10;

        (a - a) = ( 0. FX) by RLVECT_1: 15;

        then

         A2: a in q by A1, RING_1: 5, IDEAL_1: 3;

        

         XZ: x in (( RAT+ \/ [: { 0 }, RAT+ :]) \ { [ 0 , 0 ]}) by NUMBERS:def 3, RAT_1:def 2;

        

         XX: not x in RAT+

        proof

          assume x in RAT+ ;

          per cases by XBOOLE_0:def 3, ARYTM_3:def 7;

            suppose x in omega ;

            then

            reconsider n = x as Element of omega ;

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

            then

            consider m be Nat such that

             B1: a = m & m < n by A2;

            ( dom pa) = NAT by FUNCT_2:def 1;

            hence contradiction by B1;

          end;

            suppose x 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 x in { [i, j] where i,j be Element of omega : (i,j) are_coprime & j <> {} };

            then

            consider i,j be Element of omega such that

             A4: x = [i, j] & (i,j) are_coprime & j <> {} ;

            

             A5: ( dom pa) = NAT by FUNCT_2:def 1;

            pa in { {i}, {i, j}} by A2, A4, TARSKI:def 5;

            per cases by TARSKI:def 2;

              suppose pa = {i};

              hence contradiction by A5;

            end;

              suppose pa = {i, j};

              per cases by A5;

                suppose [i, (pa . i)] = i;

                hence contradiction;

              end;

                suppose [i, (pa . i)] = j;

                hence contradiction;

              end;

            end;

          end;

        end;

         not x in [: { 0 }, RAT+ :]

        proof

          assume x in [: { 0 }, RAT+ :];

          then

          consider y,z be object such that

           A4: y in { 0 } & z in RAT+ & x = [y, z] by ZFMISC_1:def 2;

          reconsider y as Element of NAT by A4, TARSKI:def 1;

          

           A5: ( dom pa) = NAT by FUNCT_2:def 1;

          pa in { {y}, {y, z}} by A2, A4, TARSKI:def 5;

          per cases by TARSKI:def 2;

            suppose pa = {y};

            hence contradiction by A5;

          end;

            suppose pa = {y, z};

            per cases by A5;

              suppose [ 0 , (pa . 0 )] = y;

              hence contradiction;

            end;

              suppose

               A7: [ 0 , (pa . 0 )] = z;

              per cases by A4, ARYTM_3:def 7, XBOOLE_0:def 3;

                suppose

                 A9: z 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 z in { [i, j] where i,j be Element of omega : (i,j) are_coprime & j <> {} };

                then

                consider i,j be Element of omega such that

                 A8: z = [i, j] & (i,j) are_coprime & j <> {} ;

                i = 0 by A7, A8, XTUPLE_0: 1;

                then j = 1 by A8, ARYTM_3: 3;

                then z in the set of all [k, 1] where k be Element of omega by A8;

                hence contradiction by A9, XBOOLE_0:def 5;

              end;

                suppose z in omega ;

                hence contradiction by A7;

              end;

            end;

          end;

        end;

        hence contradiction by XZ, XX, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    registration

      let n be Prime;

      let p be irreducible Element of the carrier of ( Polynom-Ring ( Z/ n));

      cluster ( embField ( emb p)) -> add-associative right_complementable associative distributive almost_left_invertible;

      coherence

      proof

        set F = ( Z/ n), KR = ( KroneckerField (F,p));

        

         X: ( [#] F) = the carrier of F & ( [#] KR) = the carrier of KR;

        (the carrier of F /\ the carrier of KR) = {} by Disj1;

        hence thesis by X, FIELD_2: 12, FIELD_2:def 1;

      end;

    end

    registration

      let p be irreducible Element of the carrier of ( Polynom-Ring F_Rat );

      cluster ( embField ( emb p)) -> add-associative right_complementable associative distributive almost_left_invertible;

      coherence

      proof

        set F = F_Rat , KR = ( KroneckerField (F,p));

        

         X: ( [#] F) = the carrier of F & ( [#] KR) = the carrier of KR;

        (the carrier of F /\ the carrier of ( KroneckerField (F,p))) = {} by Disj2;

        hence thesis by X, FIELD_2: 12, FIELD_2:def 1;

      end;

    end

    theorem :: FIELD_5:24

    for n be Prime, p be non constant Element of the carrier of ( Polynom-Ring ( Z/ n)) holds (( Z/ n),(( Polynom-Ring ( Z/ n)) / ( {p} -Ideal ))) are_disjoint

    proof

      let n be Prime, p be non constant Element of the carrier of ( Polynom-Ring ( Z/ n));

      set F = ( Z/ n), KR = (( Polynom-Ring ( Z/ n)) / ( {p} -Ideal ));

      

       X: ( [#] F) = the carrier of F & ( [#] KR) = the carrier of KR;

      (the carrier of ( Z/ n) /\ the carrier of (( Polynom-Ring ( Z/ n)) / ( {p} -Ideal ))) = {} by Disj1;

      hence thesis by X, FIELD_2:def 1;

    end;

    theorem :: FIELD_5:25

    for p be non constant Element of the carrier of ( Polynom-Ring F_Rat ) holds ( F_Rat ,(( Polynom-Ring F_Rat ) / ( {p} -Ideal ))) are_disjoint

    proof

      let p be non constant Element of the carrier of ( Polynom-Ring F_Rat );

      set F = F_Rat , KR = (( Polynom-Ring F_Rat ) / ( {p} -Ideal ));

      

       X: ( [#] F) = the carrier of F & ( [#] KR) = the carrier of KR;

      (the carrier of F_Rat /\ the carrier of (( Polynom-Ring F_Rat ) / ( {p} -Ideal ))) = {} by Disj2;

      hence thesis by X, FIELD_2:def 1;

    end;

    registration

      let n be Prime;

      let p be irreducible Element of the carrier of ( Polynom-Ring ( Z/ n));

      cluster ( embField ( emb p)) -> polynomial_disjoint;

      coherence

      proof

        set F = ( embField ( emb p)), FX = ( Polynom-Ring F), f = ( emb p), Kr = ( KroneckerField (( Z/ n),p));

        set o = the Element of (the carrier of F /\ the carrier of FX);

        

         X: ( [#] ( Z/ n)) = the carrier of ( Z/ n) & ( [#] Kr) = the carrier of Kr;

        

         H: the carrier of F = ( carr f) by FIELD_2:def 7

        .= ((the carrier of Kr \ ( rng f)) \/ the carrier of ( Z/ n)) by X, FIELD_2:def 2;

        now

          assume F is non polynomial_disjoint;

          then

           A1: (( [#] F) /\ ( [#] FX)) <> {} by FIELD_3:def 3;

          then

           A: o in the carrier of F & o in the carrier of FX by XBOOLE_0:def 4;

          reconsider q = o as Element of the carrier of FX by A1, XBOOLE_0:def 4;

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

          then not q in the carrier of ( Z/ n) by FIELD_3: 24;

          then o in (the carrier of Kr \ ( rng f)) by H, A, XBOOLE_0:def 3;

          then

          reconsider o as Element of (( Polynom-Ring ( Z/ n)) / ( {p} -Ideal ));

          consider a be Element of ( Polynom-Ring ( Z/ n)) such that

           B: o = ( Class (( EqRel (( Polynom-Ring ( Z/ n)),( {p} -Ideal ))),a)) by RING_1: 11;

          reconsider q as Polynomial of F;

          (a - a) = ( 0. ( Polynom-Ring ( Z/ n))) by RLVECT_1: 15;

          then

           D0: a in q by B, RING_1: 5, IDEAL_1: 3;

          then

          consider i,z be object such that

           D1: i in NAT & z in the carrier of F & a = [i, z] by ZFMISC_1:def 2;

          

           D2: z = (q . i) by D0, D1, FUNCT_1: 1;

          reconsider i as Element of NAT by D1;

          reconsider a as Polynomial of ( Z/ n) by POLYNOM3:def 10;

          ( dom a) = NAT by FUNCT_2:def 1;

          then [1, (a . 1)] in a & [2, (a . 2)] in a by FUNCT_1: 1;

          then

           E: [1, (a . 1)] in { {i}, {i, (q . i)}} & [2, (a . 2)] in { {i}, {i, (q . i)}} by D1, D2, TARSKI:def 5;

           F:

          now

            assume

             E3: i = {1};

            per cases by E, TARSKI:def 2;

              suppose [2, (a . 2)] = {i};

              then

               F1: {i} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

               {2} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

              then

               F3: {2} = {1} by E3, F1, TARSKI:def 1;

              2 in {2} by TARSKI:def 1;

              hence contradiction by F3, TARSKI:def 1;

            end;

              suppose [2, (a . 2)] = {i, (q . i)};

              then

               F1: {i, (q . i)} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

              i in {i, (q . i)} by TARSKI:def 2;

              per cases by F1, TARSKI:def 2;

                suppose

                 F3: i = {2};

                2 in {2} by TARSKI:def 1;

                hence contradiction by F3, E3, TARSKI:def 1;

              end;

                suppose

                 F3: i = {2, (a . 2)};

                2 in {2, (a . 2)} by TARSKI:def 2;

                hence contradiction by F3, E3, TARSKI:def 1;

              end;

            end;

          end;

          per cases by E, TARSKI:def 2;

            suppose [1, (a . 1)] = {i};

            then

             E1: {i} = { {1}, {1, (a . 1)}} by TARSKI:def 5;

             {1} in { {1}, {1, (a . 1)}} & {1, (a . 1)} in { {1}, {1, (a . 1)}} by TARSKI:def 2;

            hence contradiction by F, E1, TARSKI:def 1;

          end;

            suppose [1, (a . 1)] = {i, (q . i)};

            then

             E1: {i, (q . i)} = { {1}, {1, (a . 1)}} by TARSKI:def 5;

            i in {i, (q . i)} by TARSKI:def 2;

            then

             F0: i = {1, (a . 1)} by F, E1, TARSKI:def 2;

            per cases ;

              suppose

               E3: 1 = (a . 1);

              per cases by E, TARSKI:def 2;

                suppose [2, (a . 2)] = {i};

                then

                 F1: {i} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

                 {2} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

                

                then

                 F3: {2} = i by F1, TARSKI:def 1

                .= {1} by E3, F0, ENUMSET1: 29;

                2 in {2} by TARSKI:def 1;

                hence contradiction by F3, TARSKI:def 1;

              end;

                suppose [2, (a . 2)] = {i, (q . i)};

                then

                 F1: {i, (q . i)} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

                i in {i, (q . i)} by TARSKI:def 2;

                per cases by F1, TARSKI:def 2;

                  suppose i = {2};

                  then

                   F3: {2} = {1} by E3, F0, ENUMSET1: 29;

                  2 in {2} by TARSKI:def 1;

                  hence contradiction by F3, TARSKI:def 1;

                end;

                  suppose i = {2, (a . 2)};

                  then

                   F3: {1} = {2, (a . 2)} by E3, F0, ENUMSET1: 29;

                  2 in {2, (a . 2)} by TARSKI:def 2;

                  hence contradiction by F3, TARSKI:def 1;

                end;

              end;

            end;

              suppose 1 <> (a . 1);

              then

               G1: (a . 1) = 0 by F0, FIELD_3: 2;

              per cases by E, TARSKI:def 2;

                suppose [2, (a . 2)] = {i};

                then

                 F1: { {1, (a . 1)}} = { {2}, {2, (a . 2)}} by F0, TARSKI:def 5;

                 {2} in { {2}, {2, (a . 2)}} & {2, (a . 2)} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

                hence contradiction by G1, F1, CARD_1: 50;

              end;

                suppose [2, (a . 2)] = {i, (q . i)};

                then

                 F1: {2, (q . i)} = { {2}, {2, (a . 2)}} by F0, G1, TARSKI:def 5, CARD_1: 50;

                2 in {2, (q . i)} by TARSKI:def 2;

                per cases by F1, TARSKI:def 2;

                  suppose

                   F2: 2 = {2};

                  2 in {2} by TARSKI:def 1;

                  hence contradiction by F2;

                end;

                  suppose

                   F2: 2 = {2, (a . 2)};

                  2 in {2, (a . 2)} by TARSKI:def 2;

                  hence contradiction by F2;

                end;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let p be irreducible Element of the carrier of ( Polynom-Ring F_Rat );

      cluster ( embField ( emb p)) -> polynomial_disjoint;

      coherence

      proof

        set F = ( embField ( emb p)), FX = ( Polynom-Ring F), f = ( emb p), Kr = ( KroneckerField ( F_Rat ,p));

        set o = the Element of (the carrier of F /\ the carrier of FX);

        

         X: ( [#] F_Rat ) = the carrier of F_Rat & ( [#] Kr) = the carrier of Kr;

        

         H: the carrier of F = ( carr f) by FIELD_2:def 7

        .= ((the carrier of Kr \ ( rng f)) \/ the carrier of F_Rat ) by X, FIELD_2:def 2;

        now

          assume F is non polynomial_disjoint;

          then

           A1: (( [#] F) /\ ( [#] FX)) <> {} by FIELD_3:def 3;

          then

           A: o in the carrier of F & o in the carrier of FX by XBOOLE_0:def 4;

          reconsider q = o as Element of the carrier of FX by A1, XBOOLE_0:def 4;

           not q in the carrier of F_Rat by FIELD_3: 25;

          then o in (the carrier of Kr \ ( rng f)) by H, A, XBOOLE_0:def 3;

          then

          reconsider o as Element of (( Polynom-Ring F_Rat ) / ( {p} -Ideal ));

          consider a be Element of ( Polynom-Ring F_Rat ) such that

           B: o = ( Class (( EqRel (( Polynom-Ring F_Rat ),( {p} -Ideal ))),a)) by RING_1: 11;

          reconsider q as Polynomial of F;

          (a - a) = ( 0. ( Polynom-Ring F_Rat )) by RLVECT_1: 15;

          then

           D0: a in q by B, RING_1: 5, IDEAL_1: 3;

          then

          consider i,z be object such that

           D1: i in NAT & z in the carrier of F & a = [i, z] by ZFMISC_1:def 2;

          

           D2: z = (q . i) by D0, D1, FUNCT_1: 1;

          reconsider i as Element of NAT by D1;

          reconsider a as Polynomial of F_Rat by POLYNOM3:def 10;

          ( dom a) = NAT by FUNCT_2:def 1;

          then [1, (a . 1)] in a & [2, (a . 2)] in a by FUNCT_1: 1;

          then

           E: [1, (a . 1)] in { {i}, {i, (q . i)}} & [2, (a . 2)] in { {i}, {i, (q . i)}} by D1, D2, TARSKI:def 5;

           F:

          now

            assume

             E3: i = {1};

            per cases by E, TARSKI:def 2;

              suppose [2, (a . 2)] = {i};

              then

               F1: {i} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

               {2} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

              then

               F3: {2} = {1} by E3, F1, TARSKI:def 1;

              2 in {2} by TARSKI:def 1;

              hence contradiction by F3, TARSKI:def 1;

            end;

              suppose [2, (a . 2)] = {i, (q . i)};

              then

               F1: {i, (q . i)} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

              i in {i, (q . i)} by TARSKI:def 2;

              per cases by F1, TARSKI:def 2;

                suppose

                 F3: i = {2};

                2 in {2} by TARSKI:def 1;

                hence contradiction by E3, F3, TARSKI:def 1;

              end;

                suppose

                 F3: i = {2, (a . 2)};

                2 in {2, (a . 2)} by TARSKI:def 2;

                hence contradiction by E3, F3, TARSKI:def 1;

              end;

            end;

          end;

          per cases by E, TARSKI:def 2;

            suppose [1, (a . 1)] = {i};

            then

             E1: {i} = { {1}, {1, (a . 1)}} by TARSKI:def 5;

             {1} in { {1}, {1, (a . 1)}} & {1, (a . 1)} in { {1}, {1, (a . 1)}} by TARSKI:def 2;

            hence contradiction by F, E1, TARSKI:def 1;

          end;

            suppose [1, (a . 1)] = {i, (q . i)};

            then

             E1: {i, (q . i)} = { {1}, {1, (a . 1)}} by TARSKI:def 5;

            i in {i, (q . i)} by TARSKI:def 2;

            then

             F0: i = {1, (a . 1)} by F, E1, TARSKI:def 2;

            per cases ;

              suppose

               E3: 1 = (a . 1);

              per cases by E, TARSKI:def 2;

                suppose [2, (a . 2)] = {i};

                then

                 F1: {i} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

                 {2} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

                

                then

                 F3: {2} = i by F1, TARSKI:def 1

                .= {1} by E3, F0, ENUMSET1: 29;

                2 in {2} by TARSKI:def 1;

                hence contradiction by F3, TARSKI:def 1;

              end;

                suppose [2, (a . 2)] = {i, (q . i)};

                then

                 F1: {i, (q . i)} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

                i in {i, (q . i)} by TARSKI:def 2;

                per cases by F1, TARSKI:def 2;

                  suppose i = {2};

                  then

                   F3: {2} = {1} by E3, F0, ENUMSET1: 29;

                  2 in {2} by TARSKI:def 1;

                  hence contradiction by F3, TARSKI:def 1;

                end;

                  suppose i = {2, (a . 2)};

                  then

                   F3: {1} = {2, (a . 2)} by E3, F0, ENUMSET1: 29;

                  2 in {2, (a . 2)} by TARSKI:def 2;

                  hence contradiction by F3, TARSKI:def 1;

                end;

              end;

            end;

              suppose 1 <> (a . 1);

              then

               G1: (a . 1) = 0 by F0, FIELD_3: 2;

              per cases by E, TARSKI:def 2;

                suppose [2, (a . 2)] = {i};

                then

                 F1: { {1, (a . 1)}} = { {2}, {2, (a . 2)}} by F0, TARSKI:def 5;

                 {2} in { {2}, {2, (a . 2)}} & {2, (a . 2)} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

                hence contradiction by G1, F1, CARD_1: 50;

              end;

                suppose [2, (a . 2)] = {i, (q . i)};

                then

                 F1: {2, (q . i)} = { {2}, {2, (a . 2)}} by CARD_1: 50, F0, G1, TARSKI:def 5;

                2 in {2, (q . i)} by TARSKI:def 2;

                per cases by F1, TARSKI:def 2;

                  suppose

                   F2: 2 = {2};

                  2 in {2} by TARSKI:def 1;

                  hence contradiction by F2;

                end;

                  suppose

                   F2: 2 = {2, (a . 2)};

                  2 in {2, (a . 2)} by TARSKI:def 2;

                  hence contradiction by F2;

                end;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let R be Ring;

      :: FIELD_5:def4

      attr R is strong_polynomial_disjoint means

      : dspd: for a be Element of R holds for S be Ring, p be Element of the carrier of ( Polynom-Ring S) holds a <> p;

    end

    registration

      cluster INT.Ring -> strong_polynomial_disjoint;

      coherence by FIELD_3: 25;

      cluster F_Rat -> strong_polynomial_disjoint;

      coherence by FIELD_3: 25;

      cluster F_Real -> strong_polynomial_disjoint;

      coherence by FIELD_3: 26;

    end

    registration

      let n be non trivial Nat;

      cluster ( Z/ n) -> strong_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;

        hence thesis by FIELD_3: 24;

      end;

    end

    registration

      cluster strong_polynomial_disjoint -> polynomial_disjoint for Ring;

      coherence

      proof

        let R be Ring;

        assume

         A: R is strong_polynomial_disjoint;

        set o = the Element of (the carrier of R /\ the carrier of ( Polynom-Ring R));

        now

          assume not R is polynomial_disjoint;

          then (( [#] R) /\ ( [#] ( Polynom-Ring R))) <> {} by FIELD_3:def 3;

          then o in the carrier of R & o in the carrier of ( Polynom-Ring R) by XBOOLE_0:def 4;

          hence contradiction by A;

        end;

        hence thesis;

      end;

    end

    registration

      cluster strong_polynomial_disjoint for Field;

      existence

      proof

        take F_Rat ;

        thus thesis;

      end;

      cluster non strong_polynomial_disjoint for Field;

      existence

      proof

        consider F be Field such that

         A: (( [#] F) /\ ( [#] ( Polynom-Ring F))) <> {} by FIELD_3: 14;

        reconsider K = F as non polynomial_disjoint Field by A, FIELD_3:def 3;

        K is non strong_polynomial_disjoint;

        hence thesis;

      end;

    end

    theorem :: FIELD_5:26

    for F be strong_polynomial_disjoint Field, p be irreducible Element of the carrier of ( Polynom-Ring F) holds for E be Field st E = ( embField ( emb p)) holds E is strong_polynomial_disjoint

    proof

      let F be strong_polynomial_disjoint Field, p be irreducible Element of the carrier of ( Polynom-Ring F);

      let E be Field;

      assume

       AS: E = ( embField ( emb p));

      set FX = ( Polynom-Ring F), EX = ( Polynom-Ring E), f = ( emb p), Kr = ( KroneckerField (F,p));

      

       X: ( [#] F) = the carrier of F & ( [#] Kr) = the carrier of Kr;

      

       H: the carrier of E = ( carr f) by AS, FIELD_2:def 7

      .= ((the carrier of Kr \ ( rng f)) \/ the carrier of F) by X, FIELD_2:def 2;

      now

        assume E is non strong_polynomial_disjoint;

        then

        consider o be Element of E, S be Ring, q be Element of the carrier of ( Polynom-Ring S) such that

         K: o = q;

        set SX = ( Polynom-Ring S);

        per cases by H, XBOOLE_0:def 3;

          suppose o in the carrier of F;

          hence contradiction by K, dspd;

        end;

          suppose o in (the carrier of Kr \ ( rng f));

          then

          reconsider o as Element of (( Polynom-Ring F) / ( {p} -Ideal ));

          consider a be Element of ( Polynom-Ring F) such that

           B: o = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),a)) by RING_1: 11;

          reconsider q as Polynomial of S;

          (a - a) = ( 0. ( Polynom-Ring F)) by RLVECT_1: 15;

          then

           D0: a in q by K, B, RING_1: 5, IDEAL_1: 3;

          then

          consider i,z be object such that

           D1: i in NAT & z in the carrier of S & a = [i, z] by ZFMISC_1:def 2;

          

           D2: z = (q . i) by D0, D1, FUNCT_1: 1;

          reconsider i as Element of NAT by D1;

          reconsider a as Polynomial of F by POLYNOM3:def 10;

          ( dom a) = NAT by FUNCT_2:def 1;

          then [1, (a . 1)] in a & [2, (a . 2)] in a by FUNCT_1: 1;

          then

           E: [1, (a . 1)] in { {i}, {i, (q . i)}} & [2, (a . 2)] in { {i}, {i, (q . i)}} by D1, D2, TARSKI:def 5;

           F:

          now

            assume

             E3: i = {1};

            per cases by E, TARSKI:def 2;

              suppose [2, (a . 2)] = {i};

              then

               F1: {i} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

               {2} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

              then

               F3: {2} = {1} by E3, F1, TARSKI:def 1;

              2 in {2} by TARSKI:def 1;

              hence contradiction by F3, TARSKI:def 1;

            end;

              suppose [2, (a . 2)] = {i, (q . i)};

              then

               F1: {i, (q . i)} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

              i in {i, (q . i)} by TARSKI:def 2;

              per cases by F1, TARSKI:def 2;

                suppose

                 F3: i = {2};

                2 in {2} by TARSKI:def 1;

                hence contradiction by E3, F3, TARSKI:def 1;

              end;

                suppose

                 F3: i = {2, (a . 2)};

                2 in {2, (a . 2)} by TARSKI:def 2;

                hence contradiction by E3, F3, TARSKI:def 1;

              end;

            end;

          end;

          per cases by E, TARSKI:def 2;

            suppose [1, (a . 1)] = {i};

            then

             E1: {i} = { {1}, {1, (a . 1)}} by TARSKI:def 5;

             {1} in { {1}, {1, (a . 1)}} & {1, (a . 1)} in { {1}, {1, (a . 1)}} by TARSKI:def 2;

            hence contradiction by F, E1, TARSKI:def 1;

          end;

            suppose [1, (a . 1)] = {i, (q . i)};

            then

             E1: {i, (q . i)} = { {1}, {1, (a . 1)}} by TARSKI:def 5;

            i in {i, (q . i)} by TARSKI:def 2;

            then

             F0: i = {1, (a . 1)} by F, E1, TARSKI:def 2;

            per cases ;

              suppose

               E3: 1 = (a . 1);

              per cases by E, TARSKI:def 2;

                suppose [2, (a . 2)] = {i};

                then

                 F1: {i} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

                 {2} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

                

                then

                 F3: {2} = i by F1, TARSKI:def 1

                .= {1} by E3, F0, ENUMSET1: 29;

                2 in {2} by TARSKI:def 1;

                hence contradiction by F3, TARSKI:def 1;

              end;

                suppose [2, (a . 2)] = {i, (q . i)};

                then

                 F1: {i, (q . i)} = { {2}, {2, (a . 2)}} by TARSKI:def 5;

                i in {i, (q . i)} by TARSKI:def 2;

                per cases by F1, TARSKI:def 2;

                  suppose i = {2};

                  then

                   F3: {2} = {1} by E3, F0, ENUMSET1: 29;

                  2 in {2} by TARSKI:def 1;

                  hence contradiction by F3, TARSKI:def 1;

                end;

                  suppose i = {2, (a . 2)};

                  then

                   F3: {1} = {2, (a . 2)} by E3, F0, ENUMSET1: 29;

                  2 in {2, (a . 2)} by TARSKI:def 2;

                  hence contradiction by F3, TARSKI:def 1;

                end;

              end;

            end;

              suppose

               G: 1 <> (a . 1);

              

               G1: (a . 1) = 0 by F0, G, FIELD_3: 2;

              per cases by E, TARSKI:def 2;

                suppose [2, (a . 2)] = {i};

                then

                 F1: { {1, (a . 1)}} = { {2}, {2, (a . 2)}} by F0, TARSKI:def 5;

                 {2} in { {2}, {2, (a . 2)}} & {2, (a . 2)} in { {2}, {2, (a . 2)}} by TARSKI:def 2;

                hence contradiction by G1, F1, CARD_1: 50;

              end;

                suppose [2, (a . 2)] = {i, (q . i)};

                then

                 F1: {2, (q . i)} = { {2}, {2, (a . 2)}} by CARD_1: 50, F0, G1, TARSKI:def 5;

                2 in {2, (q . i)} by TARSKI:def 2;

                per cases by F1, TARSKI:def 2;

                  suppose

                   F2: 2 = {2};

                  2 in {2} by TARSKI:def 1;

                  hence contradiction by F2;

                end;

                  suppose

                   F2: 2 = {2, (a . 2)};

                  2 in {2, (a . 2)} by TARSKI:def 2;

                  hence contradiction by F2;

                end;

              end;

            end;

          end;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let X be non empty set, Z be set;

      :: FIELD_5:def5

      mode Renaming of X,Z -> Function means

      : defr: ( dom it ) = X & it is one-to-one & (( rng it ) /\ (X \/ Z)) = {} ;

      existence

      proof

        consider Y be set such that

         A: ( card (Z \/ X)) c= ( card Y) & ((Z \/ X) /\ Y) = {} by thre;

        ( card X) c= ( card (Z \/ X)) by XBOOLE_1: 7, CARD_1: 11;

        then ( card X) c= ( card Y) by A;

        then

        consider f be Function such that

         B: f is one-to-one & ( dom f) = X & ( rng f) c= Y by CARD_1: 10;

        take f;

        now

          assume

           C: (( rng f) /\ (X \/ Z)) <> {} ;

          set o = the Element of (( rng f) /\ (X \/ Z));

          o in ( rng f) & o in (X \/ Z) by C, XBOOLE_0:def 4;

          hence contradiction by A, B, XBOOLE_0:def 4;

        end;

        hence thesis by B;

      end;

    end

    registration

      let X be non empty set, Z be set;

      let r be Renaming of X, Z;

      cluster ( dom r) -> non empty;

      coherence by defr;

      cluster ( rng r) -> non empty;

      coherence

      proof

        set x = the Element of ( dom r);

        (r . x) in ( rng r) by FUNCT_1: 3;

        hence thesis;

      end;

    end

    registration

      let X be non empty set, Z be set;

      cluster -> X -defined one-to-one for Renaming of X, Z;

      coherence

      proof

        let r be Renaming of X, Z;

        ( dom r) = X by defr;

        hence r is X -defined by RELAT_1:def 18;

        thus thesis by defr;

      end;

    end

    definition

      let X be non empty set, Z be set;

      let r be Renaming of X, Z;

      :: original: "

      redefine

      func r " -> Function of ( rng r), X ;

      coherence

      proof

        ( dom r) = X by defr;

        then r is Function of X, ( rng r) by FUNCT_2: 2;

        hence thesis by FUNCT_2: 25;

      end;

    end

    theorem :: FIELD_5:27

    

     lemonto: for X be non empty set, Z be set holds for r be Renaming of X, Z holds (r " ) is onto

    proof

      let X be non empty set, Z be set;

      let r be Renaming of X, Z;

       A:

      now

        let o be object;

        assume o in X;

        then

         H: o in ( dom r) by defr;

        then (r . o) in ( rng r) by FUNCT_1: 3;

        then (r . o) in ( dom (r " )) by FUNCT_2:def 1;

        then ((r " ) . (r . o)) in ( rng (r " )) by FUNCT_1: 3;

        hence o in ( rng (r " )) by H, FUNCT_1: 34;

      end;

      now

        let o be object;

        assume o in ( rng (r " ));

        then o in ( dom r) by FUNCT_1: 33;

        hence o in X;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    definition

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      :: FIELD_5:def6

      func ren_add r -> BinOp of ( rng r) means

      : defra: for a,b be Element of ( rng r) holds (it . (a,b)) = (r . (((r " ) . a) + ((r " ) . b)));

      existence

      proof

        defpred P[ Element of ( rng r), Element of ( rng r), Element of ( rng r)] means $3 = (r . (((r " ) . $1) + ((r " ) . $2)));

         A:

        now

          let x,y be Element of ( rng r);

          set z = (r . (((r " ) . x) + ((r " ) . y)));

          ( dom r) = the carrier of F by defr;

          then z in ( rng r) by FUNCT_1: 3;

          hence ex z be Element of ( rng r) st P[x, y, z];

        end;

        consider F be BinOp of ( rng r) such that

         B: for a,b be Element of ( rng r) holds P[a, b, (F . (a,b))] from BINOP_1:sch 3( A);

        take F;

        let a,b be Element of ( rng r);

        thus thesis by B;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( rng r) such that

         A2: for a,b be Element of ( rng r) holds (F1 . (a,b)) = (r . (((r " ) . a) + ((r " ) . b))) and

         A3: for a,b be Element of ( rng r) holds (F2 . (a,b)) = (r . (((r " ) . a) + ((r " ) . b)));

        now

          let a,b be Element of ( rng r);

          

          thus (F1 . (a,b)) = (r . (((r " ) . a) + ((r " ) . b))) by A2

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

        end;

        hence thesis;

      end;

    end

    definition

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      :: FIELD_5:def7

      func ren_mult r -> BinOp of ( rng r) means

      : defrm: for a,b be Element of ( rng r) holds (it . (a,b)) = (r . (((r " ) . a) * ((r " ) . b)));

      existence

      proof

        defpred P[ Element of ( rng r), Element of ( rng r), Element of ( rng r)] means $3 = (r . (((r " ) . $1) * ((r " ) . $2)));

         A:

        now

          let x,y be Element of ( rng r);

          set z = (r . (((r " ) . x) * ((r " ) . y)));

          ( dom r) = the carrier of F by defr;

          then z in ( rng r) by FUNCT_1: 3;

          hence ex z be Element of ( rng r) st P[x, y, z];

        end;

        consider F be BinOp of ( rng r) such that

         B: for a,b be Element of ( rng r) holds P[a, b, (F . (a,b))] from BINOP_1:sch 3( A);

        take F;

        let a,b be Element of ( rng r);

        thus thesis by B;

      end;

      uniqueness

      proof

        let F1,F2 be BinOp of ( rng r) such that

         A2: for a,b be Element of ( rng r) holds (F1 . (a,b)) = (r . (((r " ) . a) * ((r " ) . b))) and

         A3: for a,b be Element of ( rng r) holds (F2 . (a,b)) = (r . (((r " ) . a) * ((r " ) . b)));

        now

          let a,b be Element of ( rng r);

          

          thus (F1 . (a,b)) = (r . (((r " ) . a) * ((r " ) . b))) by A2

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

        end;

        hence thesis;

      end;

    end

    definition

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      :: FIELD_5:def8

      func RenField r -> strict doubleLoopStr means

      : defrf: the carrier of it = ( rng r) & the addF of it = ( ren_add r) & the multF of it = ( ren_mult r) & the OneF of it = (r . ( 1. F)) & the ZeroF of it = (r . ( 0. F));

      existence

      proof

        

         H: ( dom r) = the carrier of F by defr;

        then

        reconsider e = (r . ( 1. F)) as Element of ( rng r) by FUNCT_1: 3;

        reconsider o = (r . ( 0. F)) as Element of ( rng r) by H, FUNCT_1: 3;

        take doubleLoopStr (# ( rng r), ( ren_add r), ( ren_mult r), e, o #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      cluster ( RenField r) -> non degenerated;

      coherence

      proof

        ( dom r) = the carrier of F by defr;

        then (r . ( 0. F)) <> (r . ( 1. F)) by FUNCT_1:def 4;

        then ( 0. ( RenField r)) <> (r . ( 1. F)) by defrf;

        hence thesis by defrf;

      end;

    end

    registration

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      cluster ( RenField r) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set K = ( RenField r);

        thus K is Abelian

        proof

          now

            let a,b be Element of K;

            reconsider a1 = a, b1 = b as Element of ( rng r) by defrf;

            

            thus (a + b) = (( ren_add r) . (a,b)) by defrf

            .= (r . (((r " ) . a1) + ((r " ) . b1))) by defra

            .= (( ren_add r) . (b,a)) by defra

            .= (b + a) by defrf;

          end;

          hence thesis;

        end;

        thus K is add-associative

        proof

          now

            let a,b,c be Element of K;

            reconsider a1 = a, b1 = b, c1 = c as Element of ( rng r) by defrf;

            

             H: ( dom r) = the carrier of F by defr;

            then

            reconsider ab = (r . (((r " ) . a1) + ((r " ) . b1))), bc = (r . (((r " ) . b1) + ((r " ) . c1))) as Element of ( rng r) by FUNCT_1: 3;

            

            thus ((a + b) + c) = (( ren_add r) . ((a + b),c)) by defrf

            .= (( ren_add r) . ((( ren_add r) . (a,b)),c)) by defrf

            .= (( ren_add r) . ((r . (((r " ) . a1) + ((r " ) . b1))),c)) by defra

            .= (r . (((r " ) . ab) + ((r " ) . c1))) by defra

            .= (r . ((((r " ) . a1) + ((r " ) . b1)) + ((r " ) . c1))) by H, FUNCT_1: 34

            .= (r . (((r " ) . a1) + (((r " ) . b1) + ((r " ) . c1)))) by RLVECT_1:def 3

            .= (r . (((r " ) . a1) + ((r " ) . bc))) by H, FUNCT_1: 34

            .= (( ren_add r) . (a,(r . (((r " ) . b1) + ((r " ) . c1))))) by defra

            .= (( ren_add r) . (a,(( ren_add r) . (b,c)))) by defra

            .= (( ren_add r) . (a,(b + c))) by defrf

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

          end;

          hence thesis;

        end;

        thus K is right_zeroed

        proof

          now

            let a be Element of K;

            reconsider a1 = a as Element of ( rng r) by defrf;

            

             H0: ( dom r) = the carrier of F by defr;

            then

            reconsider o = (r . ( 0. F)) as Element of ( rng r) by FUNCT_1: 3;

            

             H1: ((r " ) . (r . ( 0. F))) = ( 0. F) by H0, FUNCT_1: 34;

            

            thus (a + ( 0. K)) = (( ren_add r) . (a,( 0. K))) by defrf

            .= (( ren_add r) . (a,(r . ( 0. F)))) by defrf

            .= (r . (((r " ) . a1) + ((r " ) . o))) by defra

            .= a by H1, FUNCT_1: 35;

          end;

          hence thesis;

        end;

        thus K is right_complementable

        proof

          now

            let a be Element of K;

            reconsider a1 = a as Element of ( rng r) by defrf;

            ((r " ) . a1) is right_complementable;

            then

            consider b1 be Element of F such that

             H0: (((r " ) . a1) + b1) = ( 0. F);

            

             H1: ( rng r) = the carrier of K by defrf;

            

             H2: ( dom r) = the carrier of F by defr;

            then

            reconsider b = (r . b1) as Element of K by H1, FUNCT_1: 3;

            reconsider o = (r . b1) as Element of ( rng r) by H2, FUNCT_1: 3;

            (a + b) = (( ren_add r) . (a,b)) by defrf

            .= (r . (((r " ) . a1) + ((r " ) . o))) by defra

            .= (r . ( 0. F)) by H0, H2, FUNCT_1: 34

            .= ( 0. K) by defrf;

            hence a is right_complementable;

          end;

          hence thesis;

        end;

      end;

    end

    registration

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      cluster ( RenField r) -> commutative associative well-unital distributive almost_left_invertible;

      coherence

      proof

        set K = ( RenField r);

        thus

         C: K is commutative

        proof

          now

            let a,b be Element of K;

            reconsider a1 = a, b1 = b as Element of ( rng r) by defrf;

            

            thus (a * b) = (( ren_mult r) . (a,b)) by defrf

            .= (r . (((r " ) . a1) * ((r " ) . b1))) by defrm

            .= (r . (((r " ) . b1) * ((r " ) . a1))) by GROUP_1:def 12

            .= (( ren_mult r) . (b,a)) by defrm

            .= (b * a) by defrf;

          end;

          hence thesis;

        end;

        thus K is associative

        proof

          now

            let a,b,c be Element of K;

            reconsider a1 = a, b1 = b, c1 = c as Element of ( rng r) by defrf;

            

             H0: ( dom r) = the carrier of F by defr;

            then

            reconsider ab = (r . (((r " ) . a1) * ((r " ) . b1))), bc = (r . (((r " ) . b1) * ((r " ) . c1))) as Element of ( rng r) by FUNCT_1: 3;

            

            thus ((a * b) * c) = (( ren_mult r) . ((a * b),c)) by defrf

            .= (( ren_mult r) . ((( ren_mult r) . (a,b)),c)) by defrf

            .= (( ren_mult r) . ((r . (((r " ) . a1) * ((r " ) . b1))),c)) by defrm

            .= (r . (((r " ) . ab) * ((r " ) . c1))) by defrm

            .= (r . ((((r " ) . a1) * ((r " ) . b1)) * ((r " ) . c1))) by H0, FUNCT_1: 34

            .= (r . (((r " ) . a1) * (((r " ) . b1) * ((r " ) . c1)))) by GROUP_1:def 3

            .= (r . (((r " ) . a1) * ((r " ) . bc))) by H0, FUNCT_1: 34

            .= (( ren_mult r) . (a,(r . (((r " ) . b1) * ((r " ) . c1))))) by defrm

            .= (( ren_mult r) . (a,(( ren_mult r) . (b,c)))) by defrm

            .= (( ren_mult r) . (a,(b * c))) by defrf

            .= (a * (b * c)) by defrf;

          end;

          hence thesis;

        end;

        thus K is well-unital

        proof

          now

            let a be Element of K;

            reconsider a1 = a as Element of ( rng r) by defrf;

            

             H0: ( dom r) = the carrier of F by defr;

            then

            reconsider o = (r . ( 1. F)) as Element of ( rng r) by FUNCT_1: 3;

            

             H1: ((r " ) . (r . ( 1. F))) = ( 1. F) by H0, FUNCT_1: 34;

            

            thus (a * ( 1. K)) = (( ren_mult r) . (a,( 1. K))) by defrf

            .= (( ren_mult r) . (a,(r . ( 1. F)))) by defrf

            .= (r . (((r " ) . a1) * ((r " ) . o))) by defrm

            .= a by H1, FUNCT_1: 35;

            

            thus (( 1. K) * a) = (( ren_mult r) . (( 1. K),a)) by defrf

            .= (( ren_mult r) . ((r . ( 1. F)),a)) by defrf

            .= (r . (((r " ) . o) * ((r " ) . a1))) by defrm

            .= a by H1, FUNCT_1: 35;

          end;

          hence thesis;

        end;

        thus K is distributive

        proof

           D:

          now

            let a,b,c be Element of K;

            reconsider a1 = a, b1 = b, c1 = c as Element of ( rng r) by defrf;

            

             H: ( dom r) = the carrier of F by defr;

            then

            reconsider ab = (r . (((r " ) . a1) + ((r " ) . b1))), ac = (r . (((r " ) . a1) * ((r " ) . c1))), bc = (r . (((r " ) . b1) * ((r " ) . c1))) as Element of ( rng r) by FUNCT_1: 3;

            

            thus ((a + b) * c) = (( ren_mult r) . ((a + b),c)) by defrf

            .= (( ren_mult r) . ((( ren_add r) . (a,b)),c)) by defrf

            .= (( ren_mult r) . ((r . (((r " ) . a1) + ((r " ) . b1))),c)) by defra

            .= (r . (((r " ) . ab) * ((r " ) . c1))) by defrm

            .= (r . ((((r " ) . a1) + ((r " ) . b1)) * ((r " ) . c1))) by H, FUNCT_1: 34

            .= (r . ((((r " ) . a1) * ((r " ) . c1)) + (((r " ) . b1) * ((r " ) . c1)))) by VECTSP_1:def 7

            .= (r . (((r " ) . ac) + (((r " ) . b1) * ((r " ) . c1)))) by H, FUNCT_1: 34

            .= (r . (((r " ) . ac) + ((r " ) . bc))) by H, FUNCT_1: 34

            .= (( ren_add r) . (ac,bc)) by defra

            .= (( ren_add r) . ((r . (((r " ) . a1) * ((r " ) . c1))),(( ren_mult r) . (b,c)))) by defrm

            .= (( ren_add r) . ((( ren_mult r) . (a,c)),(( ren_mult r) . (b,c)))) by defrm

            .= (( ren_add r) . ((a * c),(( ren_mult r) . (b,c)))) by defrf

            .= (( ren_add r) . ((a * c),(b * c))) by defrf

            .= ((a * c) + (b * c)) by defrf;

          end;

          now

            let a,b,c be Element of K;

            thus ((a + b) * c) = ((a * c) + (b * c)) by D;

            

            thus (a * (b + c)) = ((b + c) * a) by C

            .= ((b * a) + (c * a)) by D

            .= ((a * b) + (c * a)) by C

            .= ((a * b) + (a * c)) by C;

          end;

          hence thesis;

        end;

        thus K is almost_left_invertible

        proof

          now

            let a be Element of K;

            assume

             AS: a <> ( 0. K);

            reconsider a1 = a as Element of ( rng r) by defrf;

            

             I0: ( dom r) = the carrier of F by defr;

            

             I1: ( rng r) = the carrier of K by defrf;

            

             I2: ( dom (r " )) = ( rng r) by FUNCT_1: 33;

            ( 0. K) = (r . ( 0. F)) by defrf;

            then ((r " ) . a1) <> ((r " ) . (r . ( 0. F))) by I1, I2, AS, FUNCT_1:def 4;

            then ((r " ) . a1) <> ( 0. F) by I0, FUNCT_1: 34;

            then ((r " ) . a1) is left_invertible by ALGSTR_0:def 39;

            then

            consider b1 be Element of F such that

             H0: (b1 * ((r " ) . a1)) = ( 1. F);

            

             H1: ( rng r) = the carrier of K by defrf;

            

             H2: ( dom r) = the carrier of F by defr;

            then

            reconsider b = (r . b1) as Element of K by H1, FUNCT_1: 3;

            reconsider o = (r . b1) as Element of ( rng r) by H2, FUNCT_1: 3;

            (b * a) = (( ren_mult r) . (b,a)) by defrf

            .= (r . (((r " ) . o) * ((r " ) . a1))) by defrm

            .= (r . ( 1. F)) by I0, H0, FUNCT_1: 34

            .= ( 1. K) by defrf;

            hence a is left_invertible;

          end;

          hence thesis;

        end;

      end;

    end

    definition

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      :: original: "

      redefine

      func r " -> Function of ( RenField r), F ;

      coherence

      proof

        

         H0: the carrier of ( RenField r) = ( rng r) by defrf

        .= ( dom (r " )) by FUNCT_1: 33;

        ( rng (r " )) = ( dom r) by FUNCT_1: 33

        .= the carrier of F by defr;

        hence thesis by H0, FUNCT_2: 1;

      end;

    end

    theorem :: FIELD_5:28

    

     thiso: for F be Field, Z be set holds for r be Renaming of the carrier of F, Z holds (r " ) is additive multiplicative unity-preserving one-to-one onto

    proof

      let F be Field, Z be set;

      let r be Renaming of the carrier of F, Z;

      set K = ( RenField r);

      

       H0: ( dom r) = the carrier of F by defr;

      now

        let a,b be Element of K;

        reconsider a1 = a, b1 = b as Element of ( rng r) by defrf;

        

        thus ((r " ) . (a + b)) = ((r " ) . (( ren_add r) . (a1,b1))) by defrf

        .= ((r " ) . (r . (((r " ) . a) + ((r " ) . b)))) by defra

        .= (((r " ) . a) + ((r " ) . b)) by H0, FUNCT_1: 34;

      end;

      hence (r " ) is additive;

      now

        let a,b be Element of K;

        reconsider a1 = a, b1 = b as Element of ( rng r) by defrf;

        

        thus ((r " ) . (a * b)) = ((r " ) . (( ren_mult r) . (a1,b1))) by defrf

        .= ((r " ) . (r . (((r " ) . a) * ((r " ) . b)))) by defrm

        .= (((r " ) . a) * ((r " ) . b)) by H0, FUNCT_1: 34;

      end;

      hence (r " ) is multiplicative;

      (r . ( 1. F)) = ( 1. K) by defrf;

      hence (r " ) is unity-preserving by H0, FUNCT_1: 34;

      thus (r " ) is one-to-one;

      thus (r " ) is onto by lemonto;

    end;

    theorem :: FIELD_5:29

    

     thisofield: for F be Field, Z be set holds ex E be Field st (E,F) are_isomorphic & (the carrier of E /\ (the carrier of F \/ Z)) = {}

    proof

      let F be Field, Z be set;

      set r = the Renaming of the carrier of F, Z;

      take E = ( RenField r);

      (r " ) is linear by thiso;

      then (r " ) is isomorphism by thiso, MOD_4:def 12;

      hence (E,F) are_isomorphic ;

      ( rng r) = the carrier of E by defrf;

      hence thesis by defr;

    end;

    begin

    

     kron: for F be Field holds for p be irreducible Element of the carrier of ( Polynom-Ring F) holds ex E be FieldExtension of F st p is_with_roots_in E

    proof

      let F be Field;

      let p be irreducible Element of the carrier of ( Polynom-Ring F);

      set KF = ( KroneckerField (F,p)), u = ( KrRoot p);

      consider FP be Field such that

       X1: (KF,FP) are_isomorphic & (the carrier of FP /\ (the carrier of KF \/ the carrier of F)) = {} by thisofield;

      

       X: ( [#] F) = the carrier of F & ( [#] FP) = the carrier of FP;

      

       X2: (F,FP) are_disjoint

      proof

        now

          assume

           A: (the carrier of F /\ the carrier of FP) <> {} ;

          set x = the Element of (the carrier of F /\ the carrier of FP);

          

           B: x in the carrier of F & x in the carrier of FP by A, XBOOLE_0:def 4;

          then x in (the carrier of KF \/ the carrier of F) by XBOOLE_0:def 3;

          hence contradiction by B, X1, XBOOLE_0:def 4;

        end;

        hence thesis by X, FIELD_2:def 1;

      end;

      consider phi be Function of KF, FP such that

       X3: phi is isomorphism by X1;

      reconsider KroneckerIsop = (( KroneckerIso p) " ) as Isomorphism of ( KroneckerField (F,p)), ( Polynom-Ring p) by RING_3: 73;

      set h = (phi * ( emb p));

      reconsider h as Function of F, FP by FUNCT_2: 13;

      

       X4: h is linear one-to-one by X3, RINGCAT1: 1;

      then

      reconsider FP as F -monomorphic Field by RING_3:def 3;

      reconsider h as Monomorphism of F, FP by X4;

      reconsider E = ( embField h) as Field by X2, FIELD_2: 12;

      ( emb_iso h) is onto by X2, FIELD_2: 15;

      then

      reconsider embisoh = (( emb_iso h) " ) as Function of FP, E by FUNCT_2: 25;

      

       Y: ( emb_iso h) is linear one-to-one onto by X2, FIELD_2: 13, FIELD_2: 14, FIELD_2: 15;

      then

      reconsider FP as E -isomorphic Field by RING_3:def 4;

      reconsider embisoh as Isomorphism of FP, E by Y, RING_3: 73;

      set iso = (embisoh * phi);

      reconsider iso as Function of KF, E by FUNCT_2: 13;

      

       X5: iso is RingHomomorphism by X3, RINGCAT1: 1;

      then

      reconsider E as KF -homomorphic Field by RING_2:def 4;

      reconsider iso as Homomorphism of KF, E by X5;

      u is_a_root_of ( emb (p,p)) by FIELD_1: 42;

      then

       Z: ( eval ((( PolyHom iso) . ( emb (p,p))),(iso . u))) = ( 0. E) by FIELD_1: 33, POLYNOM5:def 7;

      F is Subfield of E by FIELD_2: 17;

      then

      reconsider E as FieldExtension of F by FIELD_4: 7;

      take E;

      reconsider a = (iso . u) as Element of E;

      (( PolyHom iso) . ( emb (p,p))) = p

      proof

        set g = (( PolyHom iso) . ( emb (p,p)));

        

         A: for a be Element of F holds (iso . (( emb p) . a)) = a

        proof

          let a be Element of F;

          reconsider b = (a | F) as Element of the carrier of ( Polynom-Ring F) by POLYNOM3:def 10;

          reconsider v = ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),b)) as Element of ( KroneckerField (F,p)) by RING_1: 12;

          ( dom ( emb p)) = the carrier of F by FUNCT_2:def 1;

          

          then

           C: (h . a) = (phi . (( emb p) . a)) by FUNCT_1: 13

          .= (phi . v) by FIELD_1: 39;

          the carrier of ( embField h) = ( carr h) by FIELD_2:def 7

          .= ((( [#] FP) \ ( rng h)) \/ ( [#] F)) by FIELD_2:def 2

          .= ((the carrier of FP \ ( rng h)) \/ the carrier of F);

          then

          reconsider a1 = a as Element of ( embField h) by XBOOLE_0:def 3;

          a in F;

          then

           D: (( emb_iso h) . a1) = (phi . v) by C, FIELD_2:def 8;

          

           A1: ( dom phi) = the carrier of KF by FUNCT_2:def 1;

          

           A3: ( dom ( emb_iso h)) = the carrier of E by FUNCT_2:def 1;

          

          thus (iso . (( emb p) . a)) = ((embisoh * phi) . v) by FIELD_1: 39

          .= ((( emb_iso h) " ) . (phi . v)) by A1, FUNCT_1: 13

          .= a by D, A3, FUNCT_1: 34;

        end;

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Element of NAT ;

          (g . i) = (iso . (( emb (p,p)) . i)) by FIELD_1:def 2

          .= (iso . ( Class (( EqRel (( Polynom-Ring F),( {p} -Ideal ))),((p . i) | F)))) by FIELD_1: 40

          .= (iso . (( emb p) . (p . i))) by FIELD_1: 39;

          hence (g . x) = (p . x) by A;

        end;

        hence thesis;

      end;

      then ( Ext_eval (p,a)) = ( 0. E) by Z, FIELD_4: 26;

      hence thesis by FIELD_4:def 3, FIELD_4:def 2;

    end;

    theorem :: FIELD_5:30

    

     main: for F be Field holds for f be non constant Element of the carrier of ( Polynom-Ring F) holds ex E be FieldExtension of F st f is_with_roots_in E

    proof

      let F be Field;

      let f be non constant Element of the carrier of ( Polynom-Ring F);

      consider p be Element of the carrier of ( Polynom-Ring F) such that

       A: p is_a_irreducible_factor_of f by FIELD_1: 3;

      reconsider p as irreducible Element of the carrier of ( Polynom-Ring F) by A;

      consider q be Element of the carrier of ( Polynom-Ring F) such that

       B: (p * q) = f by A, GCD_1:def 1;

      consider E be FieldExtension of F such that

       C: p is_with_roots_in E by kron;

      take E;

      consider a be Element of E such that

       D: a is_a_root_of (p,E) by C, FIELD_4:def 3;

      reconsider p1 = p, q1 = q as Polynomial of F;

      

       F: F is Subring of E by FIELD_4:def 1;

      ( Ext_eval (f,a)) = ( Ext_eval ((p1 *' q1),a)) by B, POLYNOM3:def 10

      .= (( Ext_eval (p1,a)) * ( Ext_eval (q1,a))) by F, ALGNUM_1: 20

      .= (( 0. E) * ( Ext_eval (q1,a))) by D, FIELD_4:def 2;

      hence thesis by FIELD_4:def 2, FIELD_4:def 3;

    end;

    theorem :: FIELD_5:31

    for F be Field holds for f be non constant Element of the carrier of ( Polynom-Ring F) holds ex E be FieldExtension of F st f splits_in E

    proof

      let F be Field;

      let f be non constant Element of the carrier of ( Polynom-Ring F);

      defpred P[ Nat] means for F be Field holds for f be non constant Element of the carrier of ( Polynom-Ring F) st ( deg f) = $1 holds ex E be FieldExtension of F st f splits_in E;

      

       IA: P[1]

      proof

        let F be Field;

        let f be non constant Element of the carrier of ( Polynom-Ring F);

        assume

         A: ( deg f) = 1;

        reconsider E = F as FieldExtension of F by FIELD_4: 6;

        take E;

        thus thesis by FIELD_4: 29, A;

      end;

       IS:

      now

        let k be non zero Nat;

        assume

         IV: P[k];

        now

          let F be Field;

          let f be non constant Element of the carrier of ( Polynom-Ring F);

          assume

           AS2: ( deg f) = (k + 1);

          consider E1 be FieldExtension of F such that

           A: f is_with_roots_in E1 by main;

          reconsider f1 = f as Polynomial of E1 by FIELD_4: 8;

          reconsider f1 as Element of the carrier of ( Polynom-Ring E1) by POLYNOM3:def 10;

          consider a be Element of E1 such that

           B: a is_a_root_of (f,E1) by A, FIELD_4:def 3;

          reconsider h = ( rpoly (1,a)) as Element of the carrier of ( Polynom-Ring E1) by POLYNOM3:def 10;

          reconsider q = ( rpoly (1,a)) as Ppoly of E1 by RING_5: 51;

          ( Ext_eval (f,a)) = ( 0. E1) by B, FIELD_4:def 2;

          then ( 0. E1) = ( eval (f1,a)) by FIELD_4: 26;

          then

          consider g2 be Polynomial of E1 such that

           C1: f1 = (h *' g2) by RING_4: 1, RING_5: 11;

          reconsider g = g2 as Element of the carrier of ( Polynom-Ring E1) by POLYNOM3:def 10;

          

           C: f1 = (h * g) by C1, POLYNOM3:def 10;

          per cases ;

            suppose g is constant;

            then

            consider e be Element of E1 such that

             D: g = (e | E1) by RING_4: 20;

            now

              assume e is zero;

              then g = ( 0_. E1) by D, RING_4: 13;

              then f = ( 0_. F) by C1, FIELD_4: 12;

              hence contradiction;

            end;

            then

            reconsider e as non zero Element of E1;

            f = (( rpoly (1,a)) *' (e * ( 1_. E1))) by D, C1, RING_4: 16

            .= (e * (( rpoly (1,a)) *' ( 1_. E1))) by RING_4: 10

            .= (e * q);

            hence ex E be FieldExtension of F st f splits_in E by FIELD_4:def 5;

          end;

            suppose

             I: g is non constant;

            ( deg g) = k

            proof

              reconsider g1 = g as Polynomial of E1;

              g1 <> ( 0_. E1) by I;

              

              then

               D: ( deg f1) = (( deg ( rpoly (1,a))) + ( deg g1)) by C1, HURWITZ: 23

              .= (1 + ( deg g1)) by HURWITZ: 27;

              ( deg f1) = (k + 1) by AS2, FIELD_4: 20;

              hence thesis by D;

            end;

            then

            consider E2 be FieldExtension of E1 such that

             E: g splits_in E2 by I, IV;

            reconsider E2 as FieldExtension of F;

            consider e be non zero Element of E2, r be Ppoly of E2 such that

             F: g = (e * r) by E, FIELD_4:def 5;

            E1 is Subring of E2 by FIELD_4:def 1;

            then the carrier of E1 c= the carrier of E2 by C0SP1:def 3;

            then

            reconsider a1 = a as Element of E2;

            ( rpoly (1,a1)) is Ppoly of E2 by RING_5: 51;

            then

            reconsider u = (( rpoly (1,a1)) *' r) as Ppoly of E2 by RING_5: 52;

            reconsider q = ( rpoly (1,a)) as Polynomial of E2 by FIELD_4: 8;

            reconsider q1 = q as Element of the carrier of ( Polynom-Ring E2) by POLYNOM3:def 10;

            reconsider eg = (e * r) as Element of the carrier of ( Polynom-Ring E2) by POLYNOM3:def 10;

            

             Y: q = ( rpoly (1,a1)) by FIELD_4: 21;

            

             Z1: [h, g] in [:the carrier of ( Polynom-Ring E1), the carrier of ( Polynom-Ring E1):] by ZFMISC_1:def 2;

            (the multF of ( Polynom-Ring E2) || the carrier of ( Polynom-Ring E1)) = the multF of ( Polynom-Ring E1) by FIELD_4: 18;

            

            then f = (q1 * eg) by F, C, Z1, FUNCT_1: 49

            .= (q *' (e * r)) by POLYNOM3:def 10

            .= (e * u) by Y, RING_4: 10;

            hence ex E be FieldExtension of F st f splits_in E by FIELD_4:def 5;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       I: for k be non zero Nat holds P[k] from NAT_1:sch 10( IA, IS);

      consider n be Nat such that

       H: ( deg f) = n;

      (n + 1) > ( 0 + 1) by H, RING_4:def 4, XREAL_1: 6;

      hence thesis by I, H;

    end;