ring_2.miz



    begin

    definition

      let R be non empty set;

      let f be non empty FinSequence of R;

      let x be Element of ( dom f);

      :: original: .

      redefine

      func f . x -> Element of R ;

      coherence

      proof

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

        hence thesis;

      end;

    end

    registration

      let X be set;

      let F1,F2 be X -valued FinSequence;

      cluster (F1 ^ F2) -> X -valued;

      coherence

      proof

        ( rng (F1 ^ F2)) = (( rng F1) \/ ( rng F2)) by FINSEQ_1: 31;

        hence ( rng (F1 ^ F2)) c= X;

      end;

    end

    theorem :: RING_2:1

    

     prod4: for R be add-associative right_zeroed right_complementable distributive well-unital non empty doubleLoopStr, F be FinSequence of R st ex i be Nat st i in ( dom F) & (F . i) = ( 0. R) holds ( Product F) = ( 0. R)

    proof

      let R be add-associative right_zeroed right_complementable distributive well-unital non empty doubleLoopStr;

      let m be FinSequence of R;

      given i be Nat such that

       A: i in ( dom m) & (m . i) = ( 0. R);

      (m /. i) = (m . i) by A, PARTFUN1:def 6;

      hence thesis by A, POLYNOM2: 4;

    end;

    theorem :: RING_2:2

    

     prod5: for R be add-associative right_zeroed right_complementable well-unital distributive domRing-like non degenerated doubleLoopStr, F be FinSequence of R holds ( Product F) = ( 0. R) iff ex i be Nat st i in ( dom F) & (F . i) = ( 0. R)

    proof

      let R be add-associative right_zeroed right_complementable well-unital distributive domRing-like non degenerated doubleLoopStr, F be FinSequence of R;

      now

        assume

         AS: ( Product F) = ( 0. R);

        defpred P[ Nat] means for f be FinSequence of R st ( len f) = $1 holds ( Product f) = ( 0. R) implies ex i be Nat st i in ( dom f) & (f . i) = ( 0. R);

        

         A0: P[ 0 ]

        proof

          let F be FinSequence of R;

          assume ( len F) = 0 ;

          then F = ( <*> the carrier of R);

          

          then ( Product F) = ( 1_ R) by GROUP_4: 8

          .= ( 1. R);

          hence thesis;

        end;

        

         A1: for k be Nat holds P[k] implies P[(k + 1)]

        proof

          let k be Nat;

          assume

           IV: P[k];

          now

            let F be FinSequence of R;

            assume

             A3: ( len F) = (k + 1);

            then F <> {} ;

            then

            consider q be FinSequence, x be object such that

             B2: F = (q ^ <*x*>) by FINSEQ_1: 46;

            

             B2a: ( rng q) c= ( rng F) by B2, FINSEQ_1: 29;

            ( rng F) c= the carrier of R;

            then ( rng q) c= the carrier of R by B2a;

            then

            reconsider q as FinSequence of R by FINSEQ_1:def 4;

            ( rng <*x*>) = {x} by FINSEQ_1: 39;

            then

             B5: x in ( rng <*x*>) by TARSKI:def 1;

            ( rng <*x*>) c= ( rng F) by B2, FINSEQ_1: 30;

            then x in ( rng F) by B5;

            then

            reconsider x as Element of R;

            

             A4: ( len F) = (( len q) + ( len <*x*>)) by B2, FINSEQ_1: 22

            .= (( len q) + 1) by FINSEQ_1: 39;

            

             A5: ( Product F) = (( Product q) * x) by GROUP_4: 6, B2;

            assume

             A6: ( Product F) = ( 0. R);

            per cases by A6, A5, VECTSP_2:def 1;

              suppose ( Product q) = ( 0. R);

              then

              consider j be Nat such that

               C1: j in ( dom q) & (q . j) = ( 0. R) by A3, A4, IV;

              

               C2: (F . j) = (q . j) by B2, C1, FINSEQ_1:def 7;

              ( dom q) c= ( dom F) by B2, FINSEQ_1: 26;

              hence ex i be Nat st i in ( dom F) & (F . i) = ( 0. R) by C1, C2;

            end;

              suppose

               C0: x = ( 0. R);

              ( dom <*x*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

              then 1 in ( dom <*x*>) by TARSKI:def 1;

              

              then

               C1: (F . (k + 1)) = ( <*x*> . 1) by B2, A4, A3, FINSEQ_1:def 7

              .= x by FINSEQ_1:def 8;

              ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

              hence ex i be Nat st i in ( dom F) & (F . i) = ( 0. R) by C1, C0, FINSEQ_1: 4;

            end;

          end;

          hence thesis;

        end;

        

         A2: for k be Nat holds P[k] from NAT_1:sch 2( A0, A1);

        ex n be Nat st ( len F) = n;

        hence ex i be Nat st i in ( dom F) & (F . i) = ( 0. R) by AS, A2;

      end;

      hence thesis by prod4;

    end;

    definition

      let X be set;

      mode Chain of X is sequence of X;

    end

    definition

      let X be non empty set, C be Chain of X;

      :: RING_2:def1

      attr C is ascending means

      : asc: for i be Nat holds (C . i) c= (C . (i + 1));

      :: RING_2:def2

      attr C is stagnating means ex i be Nat st for j be Nat st j >= i holds (C . j) = (C . i);

    end

    registration

      let X be non empty set;

      let x be Element of X;

      cluster ( NAT --> x) -> ascending stagnating;

      coherence

      proof

        let C be Chain of X such that

         A1: C = ( NAT --> x);

        hereby

          let i be Nat;

          (C . i) = x & (C . (i + 1)) = x by A1, FUNCOP_1: 7, ORDINAL1:def 12;

          hence (C . i) c= (C . (i + 1));

        end;

        take 0 ;

        let j be Nat;

        (C . 0 ) = x & (C . j) = x by A1, FUNCOP_1: 7, ORDINAL1:def 12;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster ascending stagnating for Chain of X;

      existence

      proof

        take ( NAT --> the Element of X);

        thus thesis;

      end;

    end

    

     ch1: for X be non empty set, C be ascending Chain of X, x be object, i,j be Nat st (i <= j & x in (C . i)) holds x in (C . j)

    proof

      let X be non empty set, C be ascending Chain of X, x be object, i,j be Nat;

      assume

       AS: i <= j & x in (C . i);

      defpred P[ Nat] means for j be Nat holds j = (i + $1) implies x in (C . j);

      

       A: P[ 0 ] by AS;

       B:

      now

        let k be Nat;

        assume

         IV: P[k];

        now

          let j be Nat;

          assume

           C: j = (i + (k + 1));

          (C . (i + k)) c= (C . ((i + k) + 1)) by asc;

          hence x in (C . j) by C, IV;

        end;

        hence P[(k + 1)];

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 2( A, B);

      ex k be Nat st j = (i + k) by AS, NAT_1: 10;

      hence x in (C . j) by I;

    end;

    theorem :: RING_2:3

    for X be non empty set, C be ascending Chain of X, i,j be Nat st i <= j holds (C . i) c= (C . j) by ch1;

    definition

      let R be Ring;

      :: RING_2:def3

      func Ideals R -> Subset-Family of the carrier of R equals the set of all I where I be Ideal of R;

      coherence

      proof

        set C = the set of all I where I be Ideal of R;

        now

          let x be object;

          assume x in C;

          then ex I be Ideal of R st x = I;

          hence x in ( bool the carrier of R);

        end;

        then C c= ( bool the carrier of R);

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      cluster ( Ideals R) -> non empty;

      coherence

      proof

         {( 0. R)} in ( Ideals R);

        hence thesis;

      end;

    end

    theorem :: RING_2:4

    

     id2: for R be comRing, I be Ideal of R, a be Element of R holds a in I implies ( {a} -Ideal ) c= I

    proof

      let R be comRing, I be Ideal of R, a be Element of R;

      assume

       AS: a in I;

      now

        let x be Element of R;

        assume

         A: x in ( {a} -Ideal );

        ( {a} -Ideal ) = the set of all (a * r) where r be Element of R by IDEAL_1: 64;

        then ex r be Element of R st x = (a * r) by A;

        hence x in I by AS, IDEAL_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: RING_2:5

    

     id1: for R be Ring, C be ascending Chain of ( Ideals R) holds ( union the set of all (C . i) where i be Nat) is Ideal of R

    proof

      let R be Ring, F be ascending Chain of ( Ideals R);

      set G = the set of all (F . i) where i be Nat;

      set T = ( union G);

      

       M: (F . 0 ) in G;

      (F . 0 ) in ( Ideals R);

      then

      consider I be Ideal of R such that

       H: I = (F . 0 );

      set x = the Element of I;

      

       L: ex Y be set st x in Y & Y in G by M, H;

      now

        let x be object;

        assume x in T;

        then

        consider x1 be set such that

         H1: x in x1 & x1 in G by TARSKI:def 4;

        consider i be Nat such that

         H2: x1 = (F . i) by H1;

        (F . i) in ( Ideals R);

        hence x in the carrier of R by H1, H2;

      end;

      then T c= the carrier of R;

      then

      reconsider T as non empty Subset of R by L, TARSKI:def 4;

      now

        let x,y be Element of R;

        assume

         H0: x in T & y in T;

        then

        consider x1 be set such that

         H1: x in x1 & x1 in G by TARSKI:def 4;

        consider i be Nat such that

         H2: x1 = (F . i) by H1;

        (F . i) in ( Ideals R);

        then

        consider Ix be Ideal of R such that

         H5: Ix = (F . i);

        consider y1 be set such that

         H3: y in y1 & y1 in G by H0, TARSKI:def 4;

        consider j be Nat such that

         H4: y1 = (F . j) by H3;

        (F . j) in ( Ideals R);

        then

        consider Iy be Ideal of R such that

         H6: Iy = (F . j);

        now

          per cases ;

            suppose i <= j;

            then x in Iy by H6, H2, H1, ch1;

            hence ex Y be set st (x + y) in Y & Y in G by H3, H4, H6, IDEAL_1:def 1;

          end;

            suppose j <= i;

            then y in Ix by H5, H3, H4, ch1;

            hence ex Y be set st (x + y) in Y & Y in G by H2, H1, H5, IDEAL_1:def 1;

          end;

        end;

        hence (x + y) in T by TARSKI:def 4;

      end;

      then

       A: T is add-closed;

      now

        let p,x be Element of R;

        assume x in T;

        then

        consider x1 be set such that

         H1: x in x1 & x1 in G by TARSKI:def 4;

        consider i be Nat such that

         H2: x1 = (F . i) by H1;

        (F . i) in ( Ideals R);

        then

        consider Ix be Ideal of R such that

         H5: Ix = (F . i);

        (p * x) in Ix by H1, H2, H5, IDEAL_1:def 2;

        hence (p * x) in T by H5, H2, H1, TARSKI:def 4;

      end;

      then

       B: T is left-ideal;

      now

        let p,x be Element of R;

        assume x in T;

        then

        consider x1 be set such that

         H1: x in x1 & x1 in G by TARSKI:def 4;

        consider i be Nat such that

         H2: x1 = (F . i) by H1;

        (F . i) in ( Ideals R);

        then

        consider Ix be Ideal of R such that

         H5: Ix = (F . i);

        (x * p) in Ix by H1, H2, H5, IDEAL_1:def 3;

        hence (x * p) in T by H1, H2, H5, TARSKI:def 4;

      end;

      then T is right-ideal;

      hence thesis by A, B;

    end;

    registration

      let R be non empty doubleLoopStr, S be right_zeroed non empty doubleLoopStr;

      cluster (R --> ( 0. S)) -> additive;

      coherence

      proof

        set f = (R --> ( 0. S));

        let x,y be Element of R;

        

        thus (f . (x + y)) = ( 0. S) by FUNCOP_1: 7

        .= (( 0. S) + ( 0. S)) by RLVECT_1:def 4

        .= (( 0. S) + (f . y)) by FUNCOP_1: 7

        .= ((f . x) + (f . y)) by FUNCOP_1: 7;

      end;

    end

    registration

      let R be non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      cluster (R --> ( 0. S)) -> multiplicative;

      coherence

      proof

        set f = (R --> ( 0. S));

        let x,y be Element of R;

        

        thus ((f . x) * (f . y)) = ((f . x) * ( 0. S)) by FUNCOP_1: 7

        .= (f . (x * y)) by FUNCOP_1: 7;

      end;

    end

    registration

      let R be well-unital non empty doubleLoopStr, S be well-unital non degenerated doubleLoopStr;

      cluster (R --> ( 0. S)) -> non unity-preserving;

      coherence by FUNCOP_1: 7;

    end

    registration

      let R be non empty doubleLoopStr;

      cluster ( id R) -> additive multiplicative unity-preserving;

      coherence ;

    end

    registration

      let R be non empty doubleLoopStr;

      cluster ( id R) -> monomorphism epimorphism;

      coherence ;

    end

    registration

      let R be non empty doubleLoopStr, S be right_zeroed non empty doubleLoopStr;

      cluster additive for Function of R, S;

      existence

      proof

        take (R --> ( 0. S));

        thus thesis;

      end;

    end

    registration

      let R be non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      cluster multiplicative for Function of R, S;

      existence

      proof

        take (R --> ( 0. S));

        thus thesis;

      end;

    end

    registration

      let R,S be well-unital non empty doubleLoopStr;

      cluster unity-preserving for Function of R, S;

      existence

      proof

        deffunc F( object) = ( 1. S);

        

         A: for x be object st x in the carrier of R holds F(x) in the carrier of S;

        ex f be Function of R, S st for x be object st x in the carrier of R holds (f . x) = F(x) from FUNCT_2:sch 2( A);

        then

        consider f be Function of R, S such that

         H: for x be object st x in the carrier of R holds (f . x) = ( 1. S);

        take f;

        thus thesis by H;

      end;

    end

    registration

      let R be non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      cluster additive multiplicative for Function of R, S;

      existence

      proof

        take (R --> ( 0. S));

        thus thesis;

      end;

    end

    begin

    definition

      let R,S be Ring;

      :: RING_2:def4

      attr S is R -homomorphic means

      : defhom: ex f be Function of R, S st f is RingHomomorphism;

    end

    registration

      let R be Ring;

      cluster R -homomorphic for Ring;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

    end

    registration

      let R be comRing;

      cluster R -homomorphic for comRing;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

      cluster R -homomorphic for Ring;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Field;

      cluster R -homomorphic for Field;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

      cluster R -homomorphic for comRing;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

      cluster R -homomorphic for Ring;

      existence

      proof

        take R, ( id R);

        thus thesis;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring;

      cluster additive multiplicative unity-preserving for Function of R, S;

      existence

      proof

        consider f be Function of R, S such that

         H: f is RingHomomorphism by defhom;

        take f;

        thus thesis by H;

      end;

    end

    definition

      let R be Ring, S be R -homomorphic Ring;

      mode Homomorphism of R,S is additive multiplicative unity-preserving Function of R, S;

    end

    registration

      let R,S,T be Ring;

      let f be unity-preserving Function of R, S;

      let g be unity-preserving Function of S, T;

      cluster (g * f) -> unity-preserving;

      coherence

      proof

        now

          let x,y be Element of R;

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

          

          hence ((g * f) . ( 1. R)) = (g . (f . ( 1_ R))) by FUNCT_1: 13

          .= (g . ( 1_ S)) by GROUP_1:def 13

          .= ( 1_ T) by GROUP_1:def 13

          .= ( 1. T);

        end;

        hence thesis;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring;

      cluster -> R -homomorphic for S -homomorphic Ring;

      coherence

      proof

        let T be S -homomorphic Ring;

        set f = the Homomorphism of R, S;

        set g = the Homomorphism of S, T;

        (g * f) is Homomorphism of R, T;

        hence thesis;

      end;

    end

    notation

      let R,S be non empty doubleLoopStr;

      synonym R,S are_isomorphic for R is_ringisomorph_to S;

    end

    theorem :: RING_2:6

    

     hom1: for R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, f be additive Function of R, S holds (f . ( 0. R)) = ( 0. S)

    proof

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, f be additive Function of R, S;

      (f . ( 0. R)) = (f . (( 0. R) + ( 0. R)))

      .= ((f . ( 0. R)) + (f . ( 0. R))) by VECTSP_1:def 20;

      hence thesis by RLVECT_1: 9;

    end;

    theorem :: RING_2:7

    

     hom4a: for R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, f be additive Function of R, S holds for x be Element of R holds (f . ( - x)) = ( - (f . x))

    proof

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, f be additive Function of R, S;

      let x be Element of R;

      ( 0. S) = (f . ( 0. R)) by hom1

      .= (f . (( - x) + x)) by RLVECT_1: 5

      .= ((f . ( - x)) + (f . x)) by VECTSP_1:def 20;

      hence thesis by RLVECT_1: 6;

    end;

    theorem :: RING_2:8

    

     hom4: for R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, f be additive Function of R, S holds for x,y be Element of R holds (f . (x - y)) = ((f . x) - (f . y))

    proof

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, f be additive Function of R, S;

      let x,y be Element of R;

      

      thus (f . (x - y)) = ((f . x) + (f . ( - y))) by VECTSP_1:def 20

      .= ((f . x) - (f . y)) by hom4a;

    end;

    theorem :: RING_2:9

    

     hom2: for R be right_unital non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right_unital Abelian right-distributive domRing-like non empty doubleLoopStr, f be multiplicative Function of R, S holds (f . ( 1. R)) = ( 0. S) or (f . ( 1. R)) = ( 1. S)

    proof

      let R be right_unital non empty doubleLoopStr, S be add-associative right_zeroed right_complementable Abelian right_unital right-distributive domRing-like non empty doubleLoopStr, f be multiplicative Function of R, S;

      

       A: (f . ( 1. R)) = (f . (( 1. R) * ( 1. R)))

      .= ((f . ( 1. R)) * (f . ( 1. R))) by GROUP_6:def 6;

      

       B: ((f . ( 1. R)) * (( 1. S) - (f . ( 1. R)))) = (((f . ( 1. R)) * ( 1. S)) + ((f . ( 1. R)) * ( - (f . ( 1. R))))) by VECTSP_1:def 2

      .= (((f . ( 1. R)) * ( 1. S)) + ( - ((f . ( 1. R)) * (f . ( 1. R))))) by VECTSP_1: 8

      .= ((f . ( 1. R)) - ((f . ( 1. R)) * (f . ( 1. R))))

      .= ( 0. S) by A, RLVECT_1: 15;

      now

        assume

         C: (f . ( 1. R)) <> ( 0. S);

        

        thus (f . ( 1. R)) = ((f . ( 1. R)) + ( 0. S))

        .= ((f . ( 1. R)) + (( 1. S) + ( - (f . ( 1. R))))) by C, B, VECTSP_2:def 1

        .= (((f . ( 1. R)) + ( - (f . ( 1. R)))) + ( 1. S)) by RLVECT_1:def 3

        .= (( 0. S) + ( 1. S)) by RLVECT_1: 5

        .= ( 1. S);

      end;

      hence thesis;

    end;

    

     hom3: for E,F be Field, f be additive multiplicative Function of E, F holds ((f . ( 1. E)) = ( 0. F) & f = (E --> ( 0. F))) or ((f . ( 1. E)) = ( 1. F) & f is monomorphism)

    proof

      let E,F be Field, f be additive multiplicative Function of E, F;

      per cases by hom2;

        suppose

         A: (f . ( 1. E)) = ( 0. F);

        

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

        now

          let z be object;

          assume z in ( dom f);

          then

          reconsider x = z as Element of E;

          (f . x) = (f . (x * ( 1. E)))

          .= ((f . x) * (f . ( 1. E))) by GROUP_6:def 6

          .= ( 0. F) by A;

          hence (f . z) = ( 0. F);

        end;

        hence thesis by B, FUNCOP_1: 11;

      end;

        suppose

         A: (f . ( 1. E)) = ( 1. F);

        then

         B: f is unity-preserving;

         H:

        now

          let x be Element of E;

          assume x <> ( 0. E);

          

          then ( 1. F) = (f . (x * (x " ))) by A, VECTSP_1:def 10

          .= ((f . x) * (f . (x " ))) by GROUP_6:def 6;

          hence (f . x) <> ( 0. F);

        end;

        now

          let x,y be object;

          assume

           D: x in the carrier of E & y in the carrier of E & (f . x) = (f . y);

          then

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

          

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

          .= (( 0. E) + b) by RLVECT_1: 5

          .= b;

          then

           E: (f . b) = ((f . b) + (f . (b - a))) by D, VECTSP_1:def 20;

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

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

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

          .= (f . (b - a));

          

          then b = (a + ( 0. E)) by G, H

          .= a;

          hence x = y;

        end;

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

        hence thesis by B;

      end;

    end;

    theorem :: RING_2:10

    for E,F be Field, f be additive multiplicative Function of E, F holds (f . ( 1. E)) = ( 0. F) iff f = (E --> ( 0. F))

    proof

      let E,F be Field, f be additive multiplicative Function of E, F;

      ((f . ( 1. E)) = ( 0. F) & f = (E --> ( 0. F))) or ((f . ( 1. E)) = ( 1. F) & f is monomorphism) by hom3;

      hence thesis;

    end;

    theorem :: RING_2:11

    

     hom3a: for E,F be Field, f be additive multiplicative Function of E, F holds (f . ( 1. E)) = ( 1. F) iff f is monomorphism

    proof

      let E,F be Field, f be additive multiplicative Function of E, F;

      ((f . ( 1. E)) = ( 0. F) & f = (E --> ( 0. F))) or ((f . ( 1. E)) = ( 1. F) & f is monomorphism) by hom3;

      hence thesis;

    end;

    registration

      let E,F be Field;

      cluster additive multiplicative unity-preserving -> monomorphism for Function of E, F;

      coherence by hom3a;

    end

    definition

      let R be Ring, I be Ideal of R;

      :: RING_2:def5

      func canHom I -> Function of R, (R / I) means

      : defhomI: for a be Element of R holds (it . a) = ( Class (( EqRel (R,I)),a));

      existence

      proof

        set B = (R / I);

        defpred P[ object, object] means $2 = ( Class (( EqRel (R,I)),$1));

        

         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;

          reconsider y = ( Class (( EqRel (R,I)),a)) as Element of B by RING_1: 12;

          take y;

          thus thesis;

        end;

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

        then

        consider g be Function of R, B such that

         Y: for x be object st x in the carrier of R holds (g . x) = ( Class (( EqRel (R,I)),x));

        take g;

        thus thesis by Y;

      end;

      uniqueness

      proof

        let g1,g2 be Function of R, (R / I) such that

         A1: for a be Element of R holds (g1 . a) = ( Class (( EqRel (R,I)),a)) and

         A2: for a be Element of R holds (g2 . a) = ( Class (( EqRel (R,I)),a));

        let x be Element of R;

        

        thus (g1 . x) = ( Class (( EqRel (R,I)),x)) by A1

        .= (g2 . x) by A2;

      end;

    end

    registration

      let R be Ring, I be Ideal of R;

      cluster ( canHom I) -> additive multiplicative unity-preserving;

      coherence

      proof

        set g = ( canHom I), B = (R / I);

        now

          let a,b be Element of R;

          reconsider x = ( Class (( EqRel (R,I)),a)) as Element of B by RING_1: 12;

          reconsider y = ( Class (( EqRel (R,I)),b)) as Element of B by RING_1: 12;

          

           H1: (g . a) = ( Class (( EqRel (R,I)),a)) by defhomI;

          

           H: (x + y) = ( Class (( EqRel (R,I)),(a + b))) by RING_1: 13;

          

          thus (g . (a + b)) = (x + y) by H, defhomI

          .= ((g . a) + (g . b)) by H1, defhomI;

        end;

        hence g is additive;

        now

          let a,b be Element of R;

          reconsider x = ( Class (( EqRel (R,I)),a)) as Element of B by RING_1: 12;

          reconsider y = ( Class (( EqRel (R,I)),b)) as Element of B by RING_1: 12;

          

           H1: (g . a) = ( Class (( EqRel (R,I)),a)) by defhomI;

          

           H: (x * y) = ( Class (( EqRel (R,I)),(a * b))) by RING_1: 14;

          

          thus (g . (a * b)) = (x * y) by H, defhomI

          .= ((g . a) * (g . b)) by H1, defhomI;

        end;

        hence g is multiplicative;

        (g . ( 1. R)) = ( Class (( EqRel (R,I)),( 1. R))) by defhomI

        .= ( 1. B) by RING_1: 15;

        hence g is unity-preserving;

      end;

    end

    registration

      let R be Ring, I be Ideal of R;

      cluster ( canHom I) -> epimorphism;

      coherence

      proof

        set g = ( canHom I), B = (R / I);

        now

          let x be object;

          now

            assume x in the carrier of B;

            then

            consider a be Element of R such that

             H1: x = ( Class (( EqRel (R,I)),a)) by RING_1: 11;

            

             H2: (g . a) = x by H1, defhomI;

            ( dom g) = the carrier of R by FUNCT_2:def 1;

            hence x in ( rng g) by H2, FUNCT_1:def 3;

          end;

          hence x in ( rng g) iff x in the carrier of B;

        end;

        then g is onto by FUNCT_2:def 3, TARSKI: 2;

        hence thesis;

      end;

    end

    registration

      let R be Ring, I be Ideal of R;

      cluster (R / I) -> R -homomorphic;

      coherence

      proof

        ( canHom I) is Homomorphism of R, (R / I);

        hence thesis;

      end;

    end

    registration

      let R be add-associative right_zeroed right_complementable non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let f be additive Function of R, S;

      cluster ( ker f) -> non empty;

      coherence

      proof

        (f . ( 0. R)) = ( 0. S) by hom1;

        then ( 0. R) in ( ker f);

        hence ( ker f) is non empty;

      end;

    end

    

     ker1: for R,S be non empty doubleLoopStr, f be Function of R, S, x be Element of R st x in ( ker f) holds (f . x) = ( 0. S)

    proof

      let R,S be non empty doubleLoopStr, f be Function of R, S, x be Element of R;

      assume x in ( ker f);

      then ex y be Element of R st y = x & (f . y) = ( 0. S);

      hence thesis;

    end;

    registration

      let R be non empty doubleLoopStr, S be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let f be additive Function of R, S;

      cluster ( ker f) -> add-closed;

      coherence

      proof

        let x,y be Element of R;

        assume

         AS: x in ( ker f) & y in ( ker f);

        (f . (x + y)) = ((f . x) + (f . y)) by VECTSP_1:def 20

        .= (( 0. S) + (f . y)) by AS, ker1

        .= ( 0. S) by AS, ker1;

        hence (x + y) in ( ker f);

      end;

    end

    registration

      let R be non empty doubleLoopStr, S be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let f be multiplicative Function of R, S;

      cluster ( ker f) -> left-ideal;

      coherence

      proof

        let a,x be Element of R;

        assume

         AS: x in ( ker f);

        (f . (a * x)) = ((f . a) * (f . x)) by GROUP_6:def 6

        .= ((f . a) * ( 0. S)) by AS, ker1

        .= ( 0. S);

        hence (a * x) in ( ker f);

      end;

    end

    registration

      let R be non empty doubleLoopStr, S be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

      let f be multiplicative Function of R, S;

      cluster ( ker f) -> right-ideal;

      coherence

      proof

        let a,x be Element of R;

        assume

         AS: x in ( ker f);

        (f . (x * a)) = ((f . x) * (f . a)) by GROUP_6:def 6

        .= (( 0. S) * (f . a)) by AS, ker1

        .= ( 0. S);

        hence (x * a) in ( ker f);

      end;

    end

    registration

      let R be well-unital non empty doubleLoopStr, S be well-unital non degenerated doubleLoopStr;

      let f be unity-preserving Function of R, S;

      cluster ( ker f) -> proper;

      coherence

      proof

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

        .= ( 1. S);

        then ( ker f) <> the carrier of R by ker1;

        hence thesis by SUBSET_1:def 6;

      end;

    end

    theorem :: RING_2:12

    

     ker0: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds f is monomorphism iff ( ker f) = {( 0. R)}

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

       A:

      now

        assume

         B: f is monomorphism;

        for x be object holds x in ( ker f) iff x = ( 0. R)

        proof

          let x be object;

           C:

          now

            assume

             AS: x in ( ker f);

            then

            reconsider a = x as Element of R;

            (f . a) = ( 0. S) by AS, ker1

            .= (f . ( 0. R)) by hom1;

            hence x = ( 0. R) by B, FUNCT_2: 19;

          end;

          now

            assume

             AS: x = ( 0. R);

            then

            reconsider a = x as Element of R;

            (f . a) = ( 0. S) by AS, hom1;

            hence x in ( ker f);

          end;

          hence x in ( ker f) iff x = ( 0. R) by C;

        end;

        hence ( ker f) = {( 0. R)} by TARSKI:def 1;

      end;

      now

        assume

         AS: ( ker f) = {( 0. R)};

        now

          let x,y be object;

          assume

           AS1: x in the carrier of R & y in the carrier of R & (f . x) = (f . y);

          then

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

          ( 0. S) = ((f . a) - (f . b)) by AS1, RLVECT_1: 15

          .= (f . (a - b)) by hom4;

          then (a - b) in ( ker f);

          then ( 0. R) = (a + ( - b)) by AS, TARSKI:def 1;

          

          then a = ( - ( - b)) by RLVECT_1: 6

          .= b;

          hence x = y;

        end;

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

        hence f is monomorphism;

      end;

      hence thesis by A;

    end;

    theorem :: RING_2:13

    

     kercanhomI: for R be Ring, I be Ideal of R holds ( ker ( canHom I)) = I

    proof

      let R be Ring, I be Ideal of R;

       A:

      now

        let xx be object;

        assume

         AS: xx in ( ker ( canHom I));

        then

        reconsider x = xx as Element of R;

        ( Class (( EqRel (R,I)),( 0. R))) = ( 0. (R / I)) by RING_1:def 6

        .= (( canHom I) . x) by AS, ker1

        .= ( Class (( EqRel (R,I)),x)) by defhomI;

        then (x - ( 0. R)) in I by RING_1: 6;

        hence xx in I;

      end;

      now

        let xx be object;

        assume

         AS: xx in I;

        then

        reconsider x = xx as Element of R;

        (x - ( 0. R)) in I by AS;

        then

         B: ( Class (( EqRel (R,I)),x)) = ( Class (( EqRel (R,I)),( 0. R))) by RING_1: 6;

        (( canHom I) . x) = ( Class (( EqRel (R,I)),x)) by defhomI

        .= ( 0. (R / I)) by B, RING_1:def 6;

        hence xx in ( ker ( canHom I));

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: RING_2:14

    for R be Ring, I be Subset of R holds I is Ideal of R iff ex S be R -homomorphic Ring, f be Homomorphism of R, S st ( ker f) = I

    proof

      let R be Ring, I be Subset of R;

      now

        assume

         A: I is Ideal of R;

        thus ex S be R -homomorphic Ring, f be Homomorphism of R, S st ( ker f) = I

        proof

          reconsider I as Ideal of R by A;

          take (R / I), ( canHom I);

          thus thesis by kercanhomI;

        end;

      end;

      hence thesis;

    end;

    

     T0: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds ( 0. S) in ( rng f)

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      

       A: (f . ( 0. R)) = ( 0. S) by hom1;

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

      hence ( 0. S) in ( rng f) by A, FUNCT_1:def 3;

    end;

    

     T1: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds ( 1. S) in ( rng f)

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      

       A: (f . ( 1_ R)) = ( 1_ S) by GROUP_1:def 13

      .= ( 1. S);

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

      hence ( 1. S) in ( rng f) by A, FUNCT_1:def 3;

    end;

    

     T3: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds ( rng f) is Preserv of the addF of S

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      set F = ( rng f);

      set A = the addF of S;

      now

        let x be set;

        assume x in [:F, F:];

        then

        consider a,b be object such that

         A2: a in F and

         A3: b in F and

         A4: x = [a, b] by ZFMISC_1:def 2;

        consider a1 be Element of S such that

         A5: a1 = a & a1 in ( rng f) by A2;

        consider x1 be object such that

         A6: x1 in ( dom f) & (f . x1) = a1 by A5, FUNCT_1:def 3;

        reconsider x1 as Element of R by A6;

        consider a2 be Element of S such that

         A7: a2 = b & a2 in ( rng f) by A3;

        consider x2 be object such that

         A8: x2 in ( dom f) & (f . x2) = a2 by A7, FUNCT_1:def 3;

        reconsider x2 as Element of R by A8;

        

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

        (f . (x1 + x2)) = (a1 + a2) by A8, A6, VECTSP_1:def 20

        .= (A . x) by A4, A5, A7;

        hence (A . x) in ( rng f) by A9, FUNCT_1:def 3;

      end;

      hence thesis by REALSET1:def 1;

    end;

    

     T4: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds ( rng f) is Preserv of the multF of S

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      set F = ( rng f);

      set A = the multF of S;

      now

        let x be set;

        assume x in [:F, F:];

        then

        consider a,b be object such that

         A2: a in F and

         A3: b in F and

         A4: x = [a, b] by ZFMISC_1:def 2;

        consider a1 be Element of S such that

         A5: a1 = a & a1 in ( rng f) by A2;

        consider x1 be object such that

         A6: x1 in ( dom f) & (f . x1) = a1 by A5, FUNCT_1:def 3;

        reconsider x1 as Element of R by A6;

        consider a2 be Element of S such that

         A7: a2 = b & a2 in ( rng f) by A3;

        consider x2 be object such that

         A8: x2 in ( dom f) & (f . x2) = a2 by A7, FUNCT_1:def 3;

        reconsider x2 as Element of R by A8;

        

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

        (f . (x1 * x2)) = (a1 * a2) by A8, A6, GROUP_6:def 6

        .= (A . x) by A4, A5, A7;

        hence (A . x) in ( rng f) by A9, FUNCT_1:def 3;

      end;

      hence thesis by REALSET1:def 1;

    end;

    definition

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      :: RING_2:def6

      func Image f -> strict doubleLoopStr means

      : defim: the carrier of it = ( rng f) & the addF of it = (the addF of S || ( rng f)) & the multF of it = (the multF of S || ( rng f)) & the OneF of it = ( 1. S) & the ZeroF of it = ( 0. S);

      existence

      proof

        set A = the addF of S;

        set M = the multF of S;

        reconsider P = ( rng f) as Preserv of A by T3;

        reconsider R = ( rng f) as Preserv of M by T4;

        reconsider O = ( 1. S) as Element of P by T1;

        reconsider Z = ( 0. S) as Element of P by T0;

        reconsider MP = (M || R) as BinOp of P;

        take doubleLoopStr (# P, (A || P), MP, O, Z #);

        thus thesis;

      end;

      uniqueness ;

    end

    

     T5: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds for a,b be Element of ( Image f), x,y be Element of S st a = x & b = y holds (a + b) = (x + y) & (a * b) = (x * y)

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      let a,b be Element of ( Image f), x,y be Element of S;

      set I = ( Image f);

      the carrier of I = ( rng f) by defim;

      then

       A1: [a, b] in [:( rng f), ( rng f):] by ZFMISC_1:def 2;

      assume

       AS: a = x & b = y;

      (the addF of I . (a,b)) = ((the addF of S || ( rng f)) . (a,b)) by defim

      .= (the addF of S . (x,y)) by AS, A1, FUNCT_1: 49;

      hence (a + b) = (x + y);

      (the multF of I . (a,b)) = ((the multF of S || ( rng f)) . (a,b)) by defim

      .= (the multF of S . (x,y)) by AS, A1, FUNCT_1: 49;

      hence (a * b) = (x * y);

    end;

    

     T6: for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds for a be Element of ( Image f) holds ex x be Element of R st (f . x) = a

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      let a be Element of ( Image f);

      the carrier of ( Image f) = ( rng f) by defim;

      then ex x be object st x in ( dom f) & (f . x) = a by FUNCT_1:def 3;

      hence thesis;

    end;

    registration

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      cluster ( Image f) -> non empty;

      coherence

      proof

        ( 0. S) in ( rng f) by T0;

        hence thesis by defim;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      cluster ( Image f) -> Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        set I = ( Image f);

        now

          let v,w be Element of I;

          consider a be Element of R such that

           A1: (f . a) = v by T6;

          consider b be Element of R such that

           A2: (f . b) = w by T6;

          

          thus (v + w) = ((f . a) + (f . b)) by A1, A2, T5

          .= (w + v) by A1, A2, T5;

        end;

        hence I is Abelian;

        now

          let u,v,w be Element of I;

          consider a be Element of R such that

           A1: (f . a) = u by T6;

          consider b be Element of R such that

           A2: (f . b) = v by T6;

          consider c be Element of R such that

           A3: (f . c) = w by T6;

          

           A4: (v + w) = ((f . b) + (f . c)) by A2, A3, T5;

          (u + v) = ((f . a) + (f . b)) by A1, A2, T5;

          

          hence ((u + v) + w) = (((f . a) + (f . b)) + (f . c)) by A3, T5

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

          .= (u + (v + w)) by A1, A4, T5;

        end;

        hence I is add-associative;

        now

          let v be Element of I;

          consider a be Element of R such that

           A1: (f . a) = v by T6;

          ( 0. I) = ( 0. S) by defim;

          

          then (v + ( 0. I)) = ((f . a) + ( 0. S)) by A1, T5

          .= (f . a);

          hence (v + ( 0. I)) = v by A1;

        end;

        hence I is right_zeroed;

        now

          let x be Element of I;

          consider a be Element of R such that

           A1: (f . a) = x by T6;

          consider b be Element of R such that

           A2: (a + b) = ( 0. R) by ALGSTR_0:def 11;

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

          then (f . b) in ( rng f) by FUNCT_1: 3;

          then

          reconsider y = (f . b) as Element of I by defim;

          ( 0. I) = ( 0. S) by defim

          .= (f . ( 0. R)) by hom1

          .= ((f . a) + (f . b)) by A2, VECTSP_1:def 20

          .= (x + y) by T5, A1;

          hence x is right_complementable;

        end;

        hence I is right_complementable;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      cluster ( Image f) -> associative well-unital distributive;

      coherence

      proof

        set I = ( Image f);

        now

          let u,v,w be Element of I;

          consider a be Element of R such that

           A1: (f . a) = u by T6;

          consider b be Element of R such that

           A2: (f . b) = v by T6;

          consider c be Element of R such that

           A3: (f . c) = w by T6;

          

           A4: (v * w) = ((f . b) * (f . c)) by A2, A3, T5;

          (u * v) = ((f . a) * (f . b)) by A1, A2, T5;

          

          hence ((u * v) * w) = (((f . a) * (f . b)) * (f . c)) by A3, T5

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

          .= (u * (v * w)) by A1, A4, T5;

        end;

        hence I is associative;

        now

          let x be Element of I;

          consider a be Element of R such that

           A1: (f . a) = x by T6;

          

           A2: ( 1. S) = ( 1. I) by defim;

          

          thus (x * ( 1. I)) = ((f . a) * ( 1. S)) by A1, A2, T5

          .= x by A1;

          

          thus (( 1. I) * x) = (( 1. S) * (f . a)) by A1, A2, T5

          .= x by A1;

        end;

        hence I is well-unital;

        now

          let u,v,w be Element of I;

          consider a be Element of R such that

           A1: (f . a) = u by T6;

          consider b be Element of R such that

           A2: (f . b) = v by T6;

          consider c be Element of R such that

           A3: (f . c) = w by T6;

          

           A4: (v + w) = ((f . b) + (f . c)) by A2, A3, T5;

          

           A5: (u * v) = ((f . a) * (f . b)) by A1, A2, T5;

          

           A6: (u * w) = ((f . a) * (f . c)) by A1, A3, T5;

          

          thus (u * (v + w)) = ((f . a) * ((f . b) + (f . c))) by A1, A4, T5

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

          .= ((u * v) + (u * w)) by A5, A6, T5;

          

           A7: (v * u) = ((f . b) * (f . a)) by A1, A2, T5;

          

           A8: (w * u) = ((f . c) * (f . a)) by A1, A3, T5;

          

          thus ((v + w) * u) = (((f . b) + (f . c)) * (f . a)) by A1, A4, T5

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

          .= ((v * u) + (w * u)) by A7, A8, T5;

        end;

        hence I is distributive;

      end;

    end

    registration

      let R be comRing, S be R -homomorphic comRing, f be Homomorphism of R, S;

      cluster ( Image f) -> commutative;

      coherence

      proof

        set I = ( Image f);

        let u,v be Element of I;

        consider a be Element of R such that

         A1: (f . a) = u by T6;

        consider b be Element of R such that

         A2: (f . b) = v by T6;

        

        thus (u * v) = ((f . b) * (f . a)) by A1, A2, T5

        .= (v * u) by A1, A2, T5;

      end;

    end

    definition

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      :: original: Image

      redefine

      func Image f -> strict Subring of S ;

      coherence

      proof

        set I = ( Image f);

        

         A: the carrier of I = ( rng f) by defim;

        

         B: the addF of I = (the addF of S || the carrier of I) by A, defim;

        

         C: the multF of I = (the multF of S || the carrier of I) by A, defim;

        

         D: ( 1. I) = ( 1. S) by defim;

        ( 0. I) = ( 0. S) by defim;

        hence thesis by A, B, C, D, C0SP1:def 3;

      end;

    end

    definition

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      :: RING_2:def7

      func canHom f -> Function of (R / ( ker f)), ( Image f) means

      : ch: for a be Element of R holds (it . ( Class (( EqRel (R,( ker f))),a))) = (f . a);

      existence

      proof

        set A = (R / ( ker f)), B = ( Image f);

        defpred P[ object, object] means for a be Element of R st $1 = ( Class (( EqRel (R,( ker f))),a)) holds $2 = (f . a);

        

         X: for x be object st x in the carrier of A 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 A;

          then

          reconsider x1 = x as Element of A;

          consider b be Element of R such that

           X1: x1 = ( Class (( EqRel (R,( ker f))),b)) by RING_1: 11;

          take (f . b);

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

          then (f . b) in ( rng f) by FUNCT_1: 3;

          hence (f . b) in the carrier of B by defim;

          now

            let a be Element of R;

            assume x = ( Class (( EqRel (R,( ker f))),a));

            

            then ( 0. S) = (f . (a - b)) by ker1, X1, RING_1: 6

            .= ((f . a) - (f . b)) by hom4;

            hence (f . b) = (f . a) by RLVECT_1: 21;

          end;

          hence thesis;

        end;

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

        then

        consider g be Function of A, B such that

         Y: for x be object st x in the carrier of A holds (for a be Element of R st x = ( Class (( EqRel (R,( ker f))),a)) holds (g . x) = (f . a));

        take g;

        now

          let a be Element of R;

          reconsider x = ( Class (( EqRel (R,( ker f))),a)) as Element of A by RING_1: 12;

          x in the carrier of A;

          hence (g . ( Class (( EqRel (R,( ker f))),a))) = (f . a) by Y;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of (R / ( ker f)), ( Image f) such that

         A1: for a be Element of R holds (g1 . ( Class (( EqRel (R,( ker f))),a))) = (f . a) and

         A2: for a be Element of R holds (g2 . ( Class (( EqRel (R,( ker f))),a))) = (f . a);

        

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

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

        now

          let x be object;

          assume x in ( dom g1);

          then

          reconsider x1 = x as Element of (R / ( ker f));

          consider b be Element of R such that

           B1: x1 = ( Class (( EqRel (R,( ker f))),b)) by RING_1: 11;

          

          thus (g1 . x) = (f . b) by B1, A1

          .= (g2 . x) by B1, A2;

        end;

        hence thesis by A;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      cluster ( canHom f) -> additive multiplicative unity-preserving;

      coherence

      proof

        set g = ( canHom f), A = (R / ( ker f)), B = ( Image f), I = ( ker f);

        now

          let x,y be Element of A;

          consider a be Element of R such that

           H1: x = ( Class (( EqRel (R,I)),a)) by RING_1: 11;

          consider b be Element of R such that

           H2: y = ( Class (( EqRel (R,I)),b)) by RING_1: 11;

          

           H3: (g . x) = (f . a) by H1, ch;

          

           H4: (g . y) = (f . b) by H2, ch;

          (x + y) = ( Class (( EqRel (R,I)),(a + b))) by H1, H2, RING_1: 13;

          

          hence (g . (x + y)) = (f . (a + b)) by ch

          .= ((f . a) + (f . b)) by VECTSP_1:def 20

          .= ((g . x) + (g . y)) by H3, H4, T5;

        end;

        hence g is additive;

        now

          let x,y be Element of A;

          consider a be Element of R such that

           H1: x = ( Class (( EqRel (R,I)),a)) by RING_1: 11;

          consider b be Element of R such that

           H2: y = ( Class (( EqRel (R,I)),b)) by RING_1: 11;

          

           H3: (g . x) = (f . a) by H1, ch;

          

           H4: (g . y) = (f . b) by H2, ch;

          (x * y) = ( Class (( EqRel (R,I)),(a * b))) by H1, H2, RING_1: 14;

          

          hence (g . (x * y)) = (f . (a * b)) by ch

          .= ((f . a) * (f . b)) by GROUP_6:def 6

          .= ((g . x) * (g . y)) by H3, H4, T5;

        end;

        hence g is multiplicative;

        (g . ( 1. A)) = (g . ( Class (( EqRel (R,I)),( 1. R)))) by RING_1: 15

        .= (f . ( 1_ R)) by ch

        .= ( 1_ S) by GROUP_1:def 13

        .= ( 1. B) by defim;

        hence g is unity-preserving;

      end;

    end

    registration

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      cluster ( canHom f) -> monomorphism epimorphism;

      coherence

      proof

        set g = ( canHom f), A = (R / ( ker f)), B = ( Image f), I = ( ker f);

        now

          let x,y be object;

          assume

           D: x in the carrier of A & y in the carrier of A & (g . x) = (g . y);

          then

          reconsider x1 = x, y1 = y as Element of A;

          consider a be Element of R such that

           H1: x1 = ( Class (( EqRel (R,I)),a)) by RING_1: 11;

          consider b be Element of R such that

           H2: y1 = ( Class (( EqRel (R,I)),b)) by RING_1: 11;

          

           H3: (g . x1) = (f . a) by H1, ch;

          (f . a) = (f . b) by D, H3, H2, ch;

          

          then ( 0. S) = ((f . a) - (f . b)) by RLVECT_1: 15

          .= (f . (a - b)) by hom4;

          then (a - b) in I;

          hence x = y by H1, H2, RING_1: 6;

        end;

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

        hence g is monomorphism;

        now

          let x be object;

           Y:

          now

            assume x in ( rng g);

            then

            consider y be object such that

             H1: y in ( dom g) & (g . y) = x by FUNCT_1:def 3;

            reconsider y as Element of A by H1;

            consider a be Element of R such that

             H2: y = ( Class (( EqRel (R,I)),a)) by RING_1: 11;

            

             H3: (g . y) = (f . a) by H2, ch;

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

            hence x in ( rng f) by H1, H3, FUNCT_1: 3;

          end;

          now

            assume x in ( rng f);

            then

            consider a be object such that

             H1: a in ( dom f) & (f . a) = x by FUNCT_1:def 3;

            reconsider a as Element of R by H1;

            

             H2: (g . ( Class (( EqRel (R,I)),a))) = (f . a) by ch;

            

             H3: ( dom g) = the carrier of A by FUNCT_2:def 1;

            ( Class (( EqRel (R,I)),a)) is Element of A by RING_1: 12;

            hence x in ( rng g) by H3, H2, H1, FUNCT_1: 3;

          end;

          hence x in ( rng g) iff x in ( rng f) by Y;

        end;

        then ( rng g) = ( rng f) by TARSKI: 2;

        then ( rng g) = the carrier of B by defim;

        then g is onto by FUNCT_2:def 3;

        hence thesis;

      end;

    end

    theorem :: RING_2:15

    for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds ((R / ( ker f)),( Image f)) are_isomorphic

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      ( canHom f) is RingIsomorphism;

      hence thesis;

    end;

    theorem :: RING_2:16

    for R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S holds f is onto implies ((R / ( ker f)),S) are_isomorphic

    proof

      let R be Ring, S be R -homomorphic Ring, f be Homomorphism of R, S;

      set B = (R / ( ker f)), I = ( ker f), T = ( Image f);

      assume

       AS: f is onto;

      then

       A: ( rng f) = the carrier of S by FUNCT_2:def 3;

      

       B: ( rng ( canHom f)) = the carrier of ( Image f) by FUNCT_2:def 3

      .= ( rng f) by defim;

      then

      reconsider g = ( canHom f) as Function of B, S by FUNCT_2: 6;

       C1:

      now

        let x,y be Element of B;

        

        thus (g . (x + y)) = ((( canHom f) . x) + (( canHom f) . y)) by VECTSP_1:def 20

        .= ((the addF of S || ( rng f)) . ((( canHom f) . x),(( canHom f) . y))) by defim

        .= ((g . x) + (g . y)) by A;

      end;

       C2:

      now

        let x,y be Element of B;

        

        thus (g . (x * y)) = ((( canHom f) . x) * (( canHom f) . y)) by GROUP_6:def 6

        .= ((the multF of S || ( rng f)) . ((( canHom f) . x),(( canHom f) . y))) by defim

        .= ((g . x) * (g . y)) by A;

      end;

      (g . ( 1. B)) = (( canHom f) . ( 1_ B))

      .= ( 1_ ( Image f)) by GROUP_1:def 13

      .= ( 1. S) by defim;

      then

       C: g is additive multiplicative unity-preserving by C1, C2;

      ( rng g) = the carrier of S by B, AS, FUNCT_2:def 3;

      then g is onto by FUNCT_2:def 3;

      hence ((R / ( ker f)),S) are_isomorphic by C;

    end;

    theorem :: RING_2:17

    for R be Ring holds ((R / {( 0. R)}),R) are_isomorphic

    proof

      let R be Ring;

      ( id R) is RingHomomorphism;

      then

      reconsider S = R as R -homomorphic Ring by defhom;

      reconsider f = ( id R) as Homomorphism of R, S;

      

       A: ( ker f) = {( 0. R)} by ker0;

      set B = (R / ( ker f));

      

       B: ( rng ( canHom f)) = the carrier of ( Image f) by FUNCT_2:def 3

      .= ( rng f) by defim;

      then

      reconsider g = ( canHom f) as Function of B, S by FUNCT_2: 6;

       C1:

      now

        let x,y be Element of B;

        

        thus (g . (x + y)) = ((( canHom f) . x) + (( canHom f) . y)) by VECTSP_1:def 20

        .= ((the addF of S || ( rng f)) . ((( canHom f) . x),(( canHom f) . y))) by defim

        .= ((g . x) + (g . y));

      end;

       C2:

      now

        let x,y be Element of B;

        

        thus (g . (x * y)) = ((( canHom f) . x) * (( canHom f) . y)) by GROUP_6:def 6

        .= ((the multF of S || ( rng f)) . ((( canHom f) . x),(( canHom f) . y))) by defim

        .= ((g . x) * (g . y));

      end;

      (g . ( 1. B)) = (( canHom f) . ( 1_ B))

      .= ( 1_ ( Image f)) by GROUP_1:def 13

      .= ( 1. S) by defim;

      then

       C: g is additive multiplicative unity-preserving by C1, C2;

      g is onto by B, FUNCT_2:def 3;

      hence thesis by A, C;

    end;

    registration

      let R be Ring;

      cluster (R / ( [#] R)) -> trivial;

      coherence

      proof

        set S = (R / ( [#] R)), I = ( [#] R);

        now

          let x,y be Element of S;

          consider a be Element of R such that

           H1: x = ( Class (( EqRel (R,I)),a)) by RING_1: 11;

          consider b be Element of R such that

           H2: y = ( Class (( EqRel (R,I)),b)) by RING_1: 11;

          

          thus x = the carrier of R by H1, RING_1: 7

          .= y by H2, RING_1: 7;

        end;

        hence thesis;

      end;

    end

    begin

    registration

      let L be right_unital non empty multLoopStr;

      cluster unital for Element of L;

      existence

      proof

        ( 1. L) divides ( 1. L);

        hence thesis by GCD_1:def 2;

      end;

    end

    definition

      let L be right_unital non empty multLoopStr;

      mode Unit of L is unital Element of L;

    end

    registration

      let L be add-associative right_zeroed right_complementable left-distributive non degenerated doubleLoopStr;

      cluster non unital for Element of L;

      existence

      proof

         not ( 0. L) divides ( 1. L);

        hence thesis by GCD_1:def 2;

      end;

    end

    definition

      let L be add-associative right_zeroed right_complementable left-distributive non degenerated doubleLoopStr;

      mode NonUnit of L is non unital Element of L;

    end

    registration

      let L be add-associative right_zeroed right_complementable left-distributive non degenerated doubleLoopStr;

      cluster ( 0. L) -> non unital;

      coherence

      proof

         not ( 0. L) divides ( 1. L);

        hence thesis;

      end;

    end

    registration

      let L be right_unital non empty multLoopStr;

      cluster ( 1. L) -> unital;

      coherence

      proof

        ( 1. L) divides ( 1. L);

        hence thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable left-distributive right_unital non degenerated doubleLoopStr;

      cluster -> non zero for Unit of L;

      coherence ;

    end

    registration

      let F be Field;

      cluster -> unital for non zero Element of F;

      coherence

      proof

        let a be non zero Element of F;

        a <> ( 0. F);

        then (a * (a " )) = ( 1. F) by VECTSP_1:def 10;

        then a divides ( 1. F);

        hence a is unital;

      end;

    end

    registration

      let R be domRing, u,v be unital Element of R;

      cluster (u * v) -> unital;

      coherence

      proof

        u divides ( 1. R) by GCD_1:def 2;

        then

        consider a be Element of R such that

         H1: (u * a) = ( 1. R);

        v divides ( 1. R) by GCD_1:def 2;

        then

        consider b be Element of R such that

         H2: (v * b) = ( 1. R);

        ((b * a) * (u * v)) = (b * (a * (u * v))) by GROUP_1:def 3

        .= (b * ((a * u) * v)) by GROUP_1:def 3

        .= ( 1. R) by H2, H1;

        then (u * v) divides ( 1. R);

        hence thesis;

      end;

    end

    theorem :: RING_2:18

    

     div0: for R be comRing, a,b be Element of R holds a divides b iff b in ( {a} -Ideal )

    proof

      let R be comRing, a,b be Element of R;

       A:

      now

        assume a divides b;

        then

        consider c be Element of R such that

         A1: (a * c) = b;

        b in the set of all (a * r) where r be Element of R by A1;

        hence b in ( {a} -Ideal ) by IDEAL_1: 64;

      end;

      now

        assume b in ( {a} -Ideal );

        then b in the set of all (a * r) where r be Element of R by IDEAL_1: 64;

        then

        consider c be Element of R such that

         A1: (a * c) = b;

        thus a divides b by A1;

      end;

      hence thesis by A;

    end;

    theorem :: RING_2:19

    

     div1: for R be comRing, a,b be Element of R holds a divides b iff ( {b} -Ideal ) c= ( {a} -Ideal )

    proof

      let R be comRing, a,b be Element of R;

      now

        assume ( {b} -Ideal ) c= ( {a} -Ideal );

        then b in ( {a} -Ideal ) by IDEAL_1: 66;

        hence a divides b by div0;

      end;

      hence thesis by div0, IDEAL_1: 67;

    end;

    theorem :: RING_2:20

    

     div2: for R be comRing, a be Element of R holds a is Unit of R iff ( {a} -Ideal ) = ( [#] R)

    proof

      let R be comRing, a be Element of R;

      set A = ( {a} -Ideal );

       B:

      now

        assume a is Unit of R;

        then a divides ( 1. R) by GCD_1:def 2;

        then

        consider c be Element of R such that

         A1: (a * c) = ( 1. R);

        now

          let x be object;

          now

            assume x in the carrier of R;

            then

            reconsider x1 = x as Element of R;

            x = (x1 * (c * a)) by A1

            .= (a * (x1 * c)) by GROUP_1:def 3;

            then x in the set of all (a * r) where r be Element of R;

            hence x in A by IDEAL_1: 64;

          end;

          hence x in A iff x in the carrier of R;

        end;

        hence A = ( [#] R) by TARSKI: 2;

      end;

      now

        assume A = ( [#] R);

        then a is unital by div0;

        hence a is Unit of R;

      end;

      hence thesis by B;

    end;

    theorem :: RING_2:21

    

     div3: for R be comRing, a,b be Element of R holds a is_associated_to b iff ( {a} -Ideal ) = ( {b} -Ideal ) by div1;

    begin

    definition

      let R be right_unital non empty doubleLoopStr;

      let x be Element of R;

      :: RING_2:def8

      attr x is prime means

      : defprim: x <> ( 0. R) & not x is Unit of R & for a,b be Element of R st x divides (a * b) holds (x divides a or x divides b);

      :: RING_2:def9

      attr x is irreducible means x <> ( 0. R) & not x is Unit of R & for a be Element of R st a divides x holds (a is Unit of R or a is_associated_to x);

    end

    notation

      let R be right_unital non empty doubleLoopStr;

      let x be Element of R;

      antonym x is reducible for x is irreducible;

    end

    registration

      let R be right_unital non empty doubleLoopStr;

      cluster non prime for Element of R;

      existence

      proof

        take ( 0. R);

        thus thesis;

      end;

    end

    

     lemintr: for x,y be Integer, a,b be Element of INT.Ring st x <> 0 & x = a & y = b holds x divides y iff a divides b

    proof

      let x,y be Integer, a,b be Element of INT.Ring ;

      assume

       AS: x <> 0 & x = a & y = b;

      now

        assume x divides y;

        then

        consider z be Integer such that

         H: (x * z) = y by INT_1:def 3;

        reconsider c = z as Element of INT.Ring by INT_1:def 2, INT_3:def 3;

        (a * c) = b by H, AS;

        hence a divides b;

      end;

      hence thesis by AS, INT_1:def 3;

    end;

    registration

      cluster prime for Element of INT.Ring ;

      existence

      proof

        set R = INT.Ring ;

        set t = (( 1. R) + ( 1. R));

        reconsider x = t as Integer;

        

         A: t <> ( 0. R) by INT_3:def 3;

        

         T: not 2 divides 1 by INT_2: 13;

         not t divides ( 1. R) by T, INT_3:def 3, lemintr;

        then

         B: not t is Unit of R by GCD_1:def 2;

        now

          let a,b be Element of R;

          assume

           C1: t divides (a * b);

          reconsider y = a, z = b as Integer;

          set g = (x gcd y);

          

           C2: 2 divides (y * z) by C1, INT_3:def 3, lemintr;

          2 divides y or 2 divides z by C2, INT_5: 7, INT_2: 28;

          hence (t divides a or t divides b) by INT_3:def 3, lemintr;

        end;

        hence thesis by A, B, defprim;

      end;

    end

    registration

      let R be right_unital non empty doubleLoopStr;

      cluster prime -> non zero non unital for Element of R;

      coherence ;

      cluster irreducible -> non zero non unital for Element of R;

      coherence ;

    end

    registration

      let R be domRing;

      cluster prime -> irreducible for Element of R;

      coherence

      proof

        let x be Element of R;

        assume

         A: x is prime;

        now

          let a be Element of R;

          assume

           C: a divides x;

          then

          consider b be Element of R such that

           D: (a * b) = x;

          b <> ( 0. R) by A, D;

          then

           H: b is right_mult-cancelable by ALGSTR_0:def 37;

          now

            per cases by A, D;

              case x divides a;

              hence a is_associated_to x by C;

            end;

              case x divides b;

              then

              consider c be Element of R such that

               F: (x * c) = b;

              ((a * c) * b) = (x * c) by D, GROUP_1:def 3

              .= (( 1. R) * b) by F;

              then a divides ( 1. R) by H;

              hence a is Unit of R by GCD_1:def 2;

            end;

          end;

          hence a is Unit of R or a is_associated_to x;

        end;

        hence thesis by A;

      end;

    end

    registration

      let F be Field;

      cluster -> reducible for Element of F;

      coherence ;

    end

    definition

      let R be right_unital non empty doubleLoopStr;

      :: RING_2:def10

      func IRR R -> Subset of R equals { x where x be Element of R : x is irreducible };

      coherence

      proof

        set C = { x where x be Element of R : x is irreducible };

        now

          let y be object;

          assume y in C;

          then ex a be Element of R st a = y & a is irreducible;

          hence y in the carrier of R;

        end;

        then C c= the carrier of R;

        hence thesis;

      end;

    end

    registration

      let F be Field;

      cluster ( IRR F) -> empty;

      coherence

      proof

        set y = the Element of ( IRR F);

        assume ( IRR F) is non empty;

        then y in ( IRR F);

        then ex a be Element of F st a = y & a is irreducible;

        hence contradiction;

      end;

    end

    theorem :: RING_2:22

    

     ass0: for R be domRing, c be non zero Element of R holds for b,a,d be Element of R st (a * b) is_associated_to (c * d) & a is_associated_to c holds b is_associated_to d

    proof

      let R be domRing, c be non zero Element of R, b,a,d be Element of R;

      assume

       AS: (a * b) is_associated_to (c * d) & a is_associated_to c;

      

       H0: c <> ( 0. R);

      consider u be Element of R such that

       H1: u is unital & ((a * b) * u) = (c * d) by AS, GCD_1: 18;

      consider v be Element of R such that

       H2: v is unital & (c * v) = a by AS, GCD_1: 18;

      

       H3: (c * ((v * b) * u)) = (c * (v * (b * u))) by GROUP_1:def 3

      .= ((c * v) * (b * u)) by GROUP_1:def 3

      .= (c * d) by H1, H2, GROUP_1:def 3;

      c is right_mult-cancelable by H0, ALGSTR_0:def 37;

      

      then d = ((v * b) * u) by H3

      .= ((u * v) * b) by GROUP_1:def 3;

      hence thesis by H1, H2, GCD_1: 18;

    end;

    theorem :: RING_2:23

    

     ass1: for R be domRing, a,b be Element of R st a is irreducible & b is_associated_to a holds b is irreducible

    proof

      let R be domRing, a,b be Element of R;

      assume

       AS: a is irreducible & b is_associated_to a;

      then

      consider x be Element of R such that

       H: x is unital & (b * x) = a by GCD_1: 18;

      now

        let c be Element of R;

        assume c divides b;

        then c is Unit of R or c is_associated_to a by GCD_1: 2, AS;

        hence c is Unit of R or c is_associated_to b by AS, GCD_1: 4;

      end;

      hence thesis by AS, H;

    end;

    theorem :: RING_2:24

    

     thpr: for R be non degenerated comRing, a be non zero Element of R holds a is prime iff ( {a} -Ideal ) is prime

    proof

      let R be non degenerated comRing, a be non zero Element of R;

      set S = ( {a} -Ideal );

       A:

      now

        assume

         A0: a is prime;

        now

          let x,y be Element of R;

          assume

           A2: (x * y) in S;

          now

            per cases by A2, A0, div0;

              case a divides x;

              hence x in S by div0;

            end;

              case a divides y;

              hence y in S by div0;

            end;

          end;

          hence x in S or y in S;

        end;

        then

         B: S is quasi-prime by RING_1:def 1;

        now

          assume S is non proper;

          then S = the carrier of R by SUBSET_1:def 6;

          then a is unital by div0;

          hence contradiction by A0;

        end;

        hence S is prime by B;

      end;

      now

        assume

         A0: S is prime;

         B:

        now

          let x,y be Element of R;

          assume a divides (x * y);

          then x in S or y in S by div0, A0, RING_1:def 1;

          hence a divides x or a divides y by div0;

        end;

        now

          assume a is unital;

          then ( {( 1. R)} -Ideal ) c= S by div0, IDEAL_1: 67;

          then the carrier of R c= S by IDEAL_1: 51;

          hence contradiction by A0, SUBSET_1:def 6, XBOOLE_0:def 10;

        end;

        hence a is prime by B;

      end;

      hence thesis by A;

    end;

    theorem :: RING_2:25

    

     maxirr: for R be non degenerated comRing, a be non zero Element of R holds ( {a} -Ideal ) is maximal implies a is irreducible

    proof

      let R be non degenerated comRing, a be non zero Element of R;

      set S = ( {a} -Ideal );

      assume

       AS: S is maximal;

       B:

      now

        let x be Element of R;

        assume

         B1: x divides a;

        now

          per cases by div1, B1, AS, RING_1:def 3;

            case S = ( {x} -Ideal );

            hence x is_associated_to a by div1;

          end;

            case ( {x} -Ideal ) is non proper;

            then ( {x} -Ideal ) = the carrier of R by SUBSET_1:def 6;

            then x is unital by div0;

            hence x is Unit of R;

          end;

        end;

        hence x is Unit of R or x is_associated_to a;

      end;

      now

        assume a is unital;

        then ( {( 1. R)} -Ideal ) c= S by div0, IDEAL_1: 67;

        then the carrier of R c= S by IDEAL_1: 51;

        hence contradiction by AS, SUBSET_1:def 6, XBOOLE_0:def 10;

      end;

      hence thesis by B;

    end;

    begin

    registration

      cluster -> PID for Field;

      coherence

      proof

        let F be Field;

        let I be Ideal of F;

        per cases by IDEAL_1: 22;

          suppose I = {( 0. F)};

          then I = ( {( 0. F)} -Ideal ) by IDEAL_1: 47;

          hence thesis;

        end;

          suppose I = the carrier of F;

          then I = ( {( 1. F)} -Ideal ) by IDEAL_1: 51;

          hence thesis;

        end;

      end;

    end

    registration

      cluster PID for non empty doubleLoopStr;

      existence

      proof

        take the Field;

        thus thesis;

      end;

    end

    definition

      mode PIDomain is PID domRing;

    end

    theorem :: RING_2:26

    

     maxirr2: for R be PIDomain, a be non zero Element of R holds ( {a} -Ideal ) is maximal iff a is irreducible

    proof

      let R be PIDomain, a be non zero Element of R;

      set S = ( {a} -Ideal );

      now

        assume

         AS: a is irreducible;

        now

          let J be Ideal of R;

          assume

           H0: S c= J;

          J is principal by IDEAL_1:def 28;

          then

          consider b be Element of R such that

           H1: J = ( {b} -Ideal );

          now

            per cases by AS, H0, H1, div1;

              case b is Unit of R;

              then J = ( [#] R) by H1, div2;

              hence J is non proper;

            end;

              case b is_associated_to a;

              hence S = J by H1, div1;

            end;

          end;

          hence J = S or J is non proper;

        end;

        then

         B: S is quasi-maximal by RING_1:def 3;

        now

          assume S is non proper;

          then S = the carrier of R by SUBSET_1:def 6;

          then a is unital by div0;

          hence contradiction by AS;

        end;

        hence S is maximal by B;

      end;

      hence thesis by maxirr;

    end;

    registration

      let R be PIDomain;

      cluster irreducible -> prime for Element of R;

      coherence

      proof

        let a be Element of R;

        assume

         AS: a is irreducible;

        then ( {a} -Ideal ) is maximal by maxirr2;

        hence a is prime by AS, thpr;

      end;

    end

    registration

      cluster Euclidian -> PID for comRing;

      coherence by IDEAL_1: 94;

    end

    registration

      let R be PIDomain;

      cluster ascending -> stagnating for Chain of ( Ideals R);

      coherence

      proof

        let F be Chain of ( Ideals R);

        set G = the set of all (F . i) where i be Nat;

        assume

         AS: F is ascending;

        then

        reconsider I = ( union G) as Ideal of R by id1;

        I is principal by IDEAL_1:def 28;

        then

        consider a be Element of R such that

         H0: I = ( {a} -Ideal );

        a in I by H0, IDEAL_1: 66;

        then

        consider x1 be set such that

         H1: a in x1 & x1 in G by TARSKI:def 4;

        consider i be Nat such that

         H2: x1 = (F . i) by H1;

        (F . i) in ( Ideals R);

        then

        consider Fi be Ideal of R such that

         H3: Fi = (F . i);

        Fi c= I by H1, H2, H3, TARSKI:def 4;

        then

         B4: Fi = I by H0, H1, H2, H3, id2;

        now

          let j be Nat;

          (F . j) in ( Ideals R);

          then

          consider Fj be Ideal of R such that

           H: Fj = (F . j);

          

           B5: (F . j) in G;

          assume

           X: j >= i;

          Fj c= I by H, B5, TARSKI:def 4;

          hence (F . j) = (F . i) by B4, H, H3, H0, id2, H1, H2, ch1, AS, X;

        end;

        hence thesis;

      end;

    end

    definition

      let R be right_unital non empty doubleLoopStr;

      let x be Element of R;

      let F be non empty FinSequence of R;

      :: RING_2:def11

      pred F is_a_factorization_of x means x = ( Product F) & for i be Element of ( dom F) holds (F . i) is irreducible;

    end

    definition

      let R be right_unital non empty doubleLoopStr;

      let x be Element of R;

      :: RING_2:def12

      attr x is factorizable means ex F be non empty FinSequence of R st F is_a_factorization_of x;

    end

    definition

      let R be right_unital non empty doubleLoopStr;

      let x be Element of R;

      assume

       AS: x is factorizable;

      :: RING_2:def13

      mode Factorization of x -> non empty FinSequence of R means

      : ddf: it is_a_factorization_of x;

      existence by AS;

    end

    definition

      let R be right_unital non empty doubleLoopStr;

      let x be Element of R;

      :: RING_2:def14

      attr x is uniquely_factorizable means x is factorizable & for F,G be Factorization of x holds ex B be Function of ( dom F), ( dom G) st B is bijective & for i be Element of ( dom F) holds (G . (B . i)) is_associated_to (F . i);

    end

    registration

      let R be right_unital non empty doubleLoopStr;

      cluster uniquely_factorizable -> factorizable for Element of R;

      coherence ;

    end

    registration

      let R be domRing;

      cluster factorizable -> non zero non unital for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is factorizable;

        then

        consider F be non empty FinSequence of R such that

         AS: F is_a_factorization_of a;

        now

          assume a is zero;

          then

          consider i be Nat such that

           A: i in ( dom F) & (F . i) = ( 0. R) by AS, prod5;

          ( 0. R) is irreducible by A, AS;

          hence contradiction;

        end;

        hence a is non zero;

        ( rng F) c= the carrier of R;

        then

        reconsider f = F as Function of ( dom F), R by FUNCT_2: 2;

        now

          assume

           A1: a is unital;

          consider q be FinSequence, x be object such that

           A2: F = (q ^ <*x*>) by FINSEQ_1: 46;

          reconsider q as FinSequence of R by A2, FINSEQ_1: 36;

          ( rng <*x*>) = {x} by FINSEQ_1: 39;

          then

           A5: x in ( rng <*x*>) by TARSKI:def 1;

          

           A6: ( rng <*x*>) c= ( rng F) by A2, FINSEQ_1: 30;

          then x in ( rng F) by A5;

          then

          reconsider x as Element of R;

          a = (( Product q) * x) by GROUP_4: 6, A2, AS;

          then x divides a;

          then

           A3: x is unital by A1, GCD_1: 2;

          consider i be Nat such that

           A7: i in ( dom F) & (F . i) = x by A5, A6, FINSEQ_2: 10;

          x is irreducible by AS, A7;

          hence contradiction by A3;

        end;

        hence thesis;

      end;

    end

    

     fact1: for R be right_unital non empty doubleLoopStr, a be Element of R holds a is irreducible iff <*a*> is_a_factorization_of a

    proof

      let R be right_unital non empty doubleLoopStr, a be Element of R;

      ( rng <*a*>) c= the carrier of R;

      then

      reconsider f = <*a*> as Function of ( dom <*a*>), R by FUNCT_2: 2;

       A:

      now

        assume

         AS: a is irreducible;

        now

          let i be Element of ( dom <*a*>);

          i in ( dom <*a*>);

          then i in ( Seg 1) by FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1, FINSEQ_1: 2;

          hence ( <*a*> . i) is irreducible by AS, FINSEQ_1: 40;

        end;

        hence <*a*> is_a_factorization_of a by GROUP_4: 9;

      end;

      now

        assume

         AS: <*a*> is_a_factorization_of a;

        ( dom <*a*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

        reconsider e = 1 as Element of ( dom <*a*>) by TARSKI:def 1;

        (f . e) = a by FINSEQ_1: 40;

        hence a is irreducible by AS;

      end;

      hence thesis by A;

    end;

    registration

      let R be right_unital non empty doubleLoopStr;

      cluster irreducible -> factorizable for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is irreducible;

        then <*a*> is_a_factorization_of a by fact1;

        hence thesis;

      end;

    end

    theorem :: RING_2:27

    for R be right_unital non empty doubleLoopStr, a be Element of R holds a is irreducible iff <*a*> is_a_factorization_of a by fact1;

    theorem :: RING_2:28

    

     fact2: for R be well-unital associative non empty doubleLoopStr, a,b be Element of R, F,G be non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds (F ^ G) is_a_factorization_of (a * b)

    proof

      let R be well-unital associative non empty doubleLoopStr, a,b be Element of R, F,G be non empty FinSequence of R;

      assume

       AS: F is_a_factorization_of a & G is_a_factorization_of b;

      reconsider FG = (F ^ G) as non empty FinSequence of R;

      ( rng F) c= the carrier of R;

      then

      reconsider f = F as Function of ( dom F), R by FUNCT_2: 2;

      ( rng G) c= the carrier of R;

      then

      reconsider g = G as Function of ( dom G), R by FUNCT_2: 2;

      ( rng FG) c= the carrier of R;

      then

      reconsider fg = FG as Function of ( dom FG), R by FUNCT_2: 2;

      now

        let i be Element of ( dom (F ^ G));

        now

          per cases by FINSEQ_1: 25;

            suppose

             B: i in ( dom F);

            (fg . i) = (f . i) by B, FINSEQ_1:def 7;

            hence ((F ^ G) . i) is irreducible by B, AS;

          end;

            suppose ex n be Nat st n in ( dom G) & i = (( len F) + n);

            then

            consider n be Nat such that

             B: n in ( dom G) & i = (( len F) + n);

            (fg . i) = (g . n) by B, FINSEQ_1:def 7;

            hence ((F ^ G) . i) is irreducible by B, AS;

          end;

        end;

        hence ((F ^ G) . i) is irreducible;

      end;

      hence thesis by AS, GROUP_4: 5;

    end;

    

     lemfactunique1: for R be domRing, a,b,x be Element of R, F be non empty FinSequence of R st x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b holds ex i be Element of ( dom F) st (F . i) is_associated_to x

    proof

      let R be domRing, a,b,x be Element of R, F be non empty FinSequence of R;

      assume

       AS: x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b;

      defpred P[ Nat] means for F be non empty FinSequence of R, a,b be Element of R st ( len F) = $1 & x divides a & a is_associated_to b & F is_a_factorization_of b holds ex i be Element of ( dom F) st (F . i) is_associated_to x;

      

       A0: P[ 0 ];

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         IV: P[k];

        now

          let F be non empty FinSequence of R, a,b be Element of R;

          assume

           A3: ( len F) = (k + 1) & x divides a & a is_associated_to b & F is_a_factorization_of b;

          consider q be FinSequence, y be object such that

           B2: F = (q ^ <*y*>) by FINSEQ_1: 46;

          

           B2a: ( rng q) c= ( rng F) by B2, FINSEQ_1: 29;

          ( rng F) c= the carrier of R;

          then ( rng q) c= the carrier of R by B2a;

          then

          reconsider q as FinSequence of R by FINSEQ_1:def 4;

          ( rng <*y*>) = {y} by FINSEQ_1: 39;

          then

           B5: y in ( rng <*y*>) by TARSKI:def 1;

          ( rng <*y*>) c= ( rng F) by B2, FINSEQ_1: 30;

          then y in ( rng F) by B5;

          then

          reconsider y as Element of R;

          

           A4: ( len F) = (( len q) + ( len <*y*>)) by B2, FINSEQ_1: 22

          .= (( len q) + 1) by FINSEQ_1: 39;

          

           A5: b = (( Product q) * y) by GROUP_4: 6, B2, A3;

          ( dom <*y*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

          then 1 in ( dom <*y*>) by TARSKI:def 1;

          

          then

           A6: (F . (k + 1)) = ( <*y*> . 1) by B2, A4, A3, FINSEQ_1:def 7

          .= y by FINSEQ_1:def 8;

          ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

          then

           A8: (k + 1) in ( dom F) by FINSEQ_1: 4;

          then

           A7: y is irreducible by A6, A3;

          consider d be Element of R such that

           Z: d is unital & (a * d) = b by A3, GCD_1: 18;

          

           A9: x divides b by Z, A3, GCD_1: 7;

          per cases by A5, A9, AS;

            suppose x divides y;

            then x is_associated_to y by AS, A7;

            hence ex i be Element of ( dom F) st (F . i) is_associated_to x by A8, A6;

          end;

            suppose

             C0: x divides ( Product q);

            now

              per cases ;

                suppose q = {} ;

                

                then b = ( Product <*y*>) by A3, B2, FINSEQ_1: 34

                .= y by GROUP_4: 9;

                then x is_associated_to y by AS, A7, Z, A3, GCD_1: 7;

                hence ex i be Element of ( dom F) st (F . i) is_associated_to x by A6, A8;

              end;

                suppose q <> {} ;

                then

                reconsider q as non empty FinSequence of R;

                now

                  let i be Element of ( dom q);

                  ( dom q) c= ( dom F) by B2, FINSEQ_1: 26;

                  then

                  reconsider j = i as Element of ( dom F);

                  (F . j) is irreducible by A3;

                  hence (q . i) is irreducible by B2, FINSEQ_1:def 7;

                end;

                then q is_a_factorization_of ( Product q);

                then

                consider i be Element of ( dom q) such that

                 C1: (q . i) is_associated_to x by IV, C0, A3, A4;

                

                 C3: (F . i) = (q . i) by B2, FINSEQ_1:def 7;

                ( dom q) c= ( dom F) by B2, FINSEQ_1: 26;

                then i in ( dom F);

                hence ex i be Element of ( dom F) st (F . i) is_associated_to x by C1, C3;

              end;

            end;

            hence ex i be Element of ( dom F) st (F . i) is_associated_to x;

          end;

        end;

        hence thesis;

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 2( A0, A1);

      ex n be Nat st ( len F) = n;

      hence thesis by I, AS;

    end;

    

     lemfactunique: for R be PIDomain, x,y be Element of R holds for F,G be non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds ex p be Function of ( dom F), ( dom G) st p is bijective & for i be Element of ( dom F) holds (G . (p . i)) is_associated_to (F . i)

    proof

      let R be PIDomain, x,y be Element of R;

      let F,G be non empty FinSequence of R;

      assume

       AS: F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y;

      defpred P[ Nat] means for x,y be Element of R holds for F,G be non empty FinSequence of R st ( len F) = $1 & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds ( len G) = $1 & ex p be Function of ( dom F), ( dom G) st p is bijective & for i be Element of ( dom F) holds (G . (p . i)) is_associated_to (F . i);

      

       A0: P[ 0 ];

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         IV: P[k];

        now

          let x,y be Element of R;

          let F,G be non empty FinSequence of R;

          assume

           A3: ( len F) = (k + 1) & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y;

          consider F1 be FinSequence, a be object such that

           B2: F = (F1 ^ <*a*>) by FINSEQ_1: 46;

          

           B2a: ( rng F1) c= ( rng F) by B2, FINSEQ_1: 29;

          ( rng F) c= the carrier of R;

          then ( rng F1) c= the carrier of R by B2a;

          then

          reconsider F1 as FinSequence of R by FINSEQ_1:def 4;

          ( rng <*a*>) = {a} by FINSEQ_1: 39;

          then

           B5: a in ( rng <*a*>) by TARSKI:def 1;

          ( rng <*a*>) c= ( rng F) by B2, FINSEQ_1: 30;

          then a in ( rng F) by B5;

          then

          reconsider a as Element of R;

          

           A4: ( len F) = (( len F1) + ( len <*a*>)) by B2, FINSEQ_1: 22

          .= (( len F1) + 1) by FINSEQ_1: 39;

          ( dom <*a*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

          then 1 in ( dom <*a*>) by TARSKI:def 1;

          

          then

           A6: (F . (k + 1)) = ( <*a*> . 1) by B2, A4, A3, FINSEQ_1:def 7

          .= a by FINSEQ_1:def 8;

          ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

          then

           A7: (k + 1) in ( dom F) by FINSEQ_1: 4;

          then

           A7a: a is irreducible by A6, A3;

          

           A10: ( Product F) = (( Product F1) * a) by B2, GROUP_4: 6;

          consider r be FinSequence, b be object such that

           G2: G = (r ^ <*b*>) by FINSEQ_1: 46;

          

           G2a: ( rng r) c= ( rng G) by G2, FINSEQ_1: 29;

          ( rng G) c= the carrier of R;

          then ( rng r) c= the carrier of R by G2a;

          then

          reconsider r as FinSequence of R by FINSEQ_1:def 4;

          ( rng <*b*>) = {b} by FINSEQ_1: 39;

          then

           G5: b in ( rng <*b*>) by TARSKI:def 1;

          ( rng <*b*>) c= ( rng G) by G2, FINSEQ_1: 30;

          then b in ( rng G) by G5;

          then

          reconsider b as Element of R;

          ( dom <*b*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

          then 1 in ( dom <*b*>) by TARSKI:def 1;

          

          then

           G6: (G . (( len r) + 1)) = ( <*b*> . 1) by G2, FINSEQ_1:def 7

          .= b by FINSEQ_1:def 8;

          

           G12: ( len G) = (( len r) + ( len <*b*>)) by G2, FINSEQ_1: 22

          .= (( len r) + 1) by FINSEQ_1: 39;

          then ( dom G) = ( Seg (( len r) + 1)) by FINSEQ_1:def 3;

          then (( len r) + 1) in ( dom G) by FINSEQ_1: 4;

          then

           G7: b is irreducible by G6, A3;

          then

           G11: b is right_mult-cancelable by ALGSTR_0:def 37;

          

           G9: ( Product G) = (( Product r) * b) by G2, GROUP_4: 6;

          then

           G10: b divides y by A3;

          per cases ;

            suppose F1 = {} ;

            then

             C1: F = <*a*> by B2, FINSEQ_1: 34;

            then

             C2: ( len F) = 1 by FINSEQ_1: 40;

            

             C5: x = a by A3, C1, GROUP_4: 9;

            then

             D1: y is irreducible by A3, A7, A6, ass1;

             C3:

            now

              assume ( len G) <> ( len F);

              then

              reconsider r as non empty FinSequence of R by G12, C1, FINSEQ_1: 40;

              consider u be Element of R such that

               C4: u is unital & (b * u) = y by D1, G7, G10, GCD_1: 18;

              ( Product r) is factorizable

              proof

                take r;

                thus ( Product r) = ( Product r);

                let i be Element of ( dom r);

                ( dom r) c= ( dom G) by G2, FINSEQ_1: 26;

                then

                reconsider j = i as Element of ( dom G);

                (G . j) is irreducible by A3;

                hence thesis by G2, FINSEQ_1:def 7;

              end;

              hence contradiction by A3, G9, C4, G11;

            end;

            then

             C7: G = <*(G . 1)*> by C2, FINSEQ_1: 40;

            then

             C4: ( dom G) = ( Seg 1) & ( dom F) = ( Seg 1) by FINSEQ_1: 38, C1;

            then

            reconsider p = ( id ( dom F)) as Function of ( dom F), ( dom G);

            now

              let i be Element of ( dom F);

              

               E0: i = 1 by C4, TARSKI:def 1, FINSEQ_1: 2;

              then (F . i) = a by C1, FINSEQ_1: 40;

              hence (G . (p . i)) is_associated_to (F . i) by E0, A3, C5, C7, GROUP_4: 9;

            end;

            hence ( len G) = (k + 1) & ex p be Function of ( dom F), ( dom G) st p is bijective & for i be Element of ( dom F) holds (G . (p . i)) is_associated_to (F . i) by A3, C4, C3;

          end;

            suppose F1 <> {} ;

            then

            reconsider F1 as non empty FinSequence of R;

            a divides ( Product F) by A10;

            then

            consider j be Element of ( dom G) such that

             E1: (G . j) is_associated_to a by lemfactunique1, A3, A7a;

            ( rng G) c= the carrier of R;

            then

            reconsider g = G as Function of ( dom G), R by FUNCT_2: 2;

            

             E3: (g . j) = (g /. j);

            set G1 = ( Del (G,j));

            consider lg1 be Nat such that

             LG1: ( len G) = (lg1 + 1) & ( len G1) = lg1 by FINSEQ_3: 104;

            

             LG3: ( dom G) = ( Seg (lg1 + 1)) & ( dom G1) = ( Seg lg1) by LG1, FINSEQ_1:def 3;

            then

             LG2: ( dom G1) c= ( dom G) by NAT_1: 11, FINSEQ_1: 5;

            ( Product G) = ((G . j) * ( Product G1)) by E3, RATFUNC1: 3;

            then (a * ( Product F1)) is_associated_to ((G . j) * ( Product G1)) by A3, B2, GROUP_4: 6;

            then

             I0: ( Product F1) is_associated_to ( Product G1) by A7a, E1, ass0;

            now

              let i be Element of ( dom F1);

              ( dom F1) c= ( dom F) by B2, FINSEQ_1: 26;

              then

              reconsider j = i as Element of ( dom F);

              (F . j) is irreducible by A3;

              hence (F1 . i) is irreducible by B2, FINSEQ_1:def 7;

            end;

            then

             I1: F1 is_a_factorization_of ( Product F1);

            now

              assume G1 = {} ;

              then G1 = ( <*> the carrier of R);

              then ( Product F1) is_associated_to ( 1_ R) by I0, GROUP_4: 8;

              then ( Product F1) is unital factorizable by I1;

              hence contradiction;

            end;

            then

            reconsider G1 as non empty FinSequence of R;

            now

              let i be Element of ( dom G1);

              i in ( dom G1);

              then i in ( Seg lg1) by LG1, FINSEQ_1:def 3;

              then

               H1: 1 <= i & i <= lg1 by FINSEQ_1: 1;

              per cases ;

                suppose

                 G: i < j;

                lg1 <= (lg1 + 1) by NAT_1: 11;

                then i <= (lg1 + 1) by H1, XXREAL_0: 2;

                then i in ( Seg (lg1 + 1)) by H1;

                then

                reconsider ii = i as Element of ( dom G) by LG1, FINSEQ_1:def 3;

                (G . ii) is irreducible by A3;

                hence (G1 . i) is irreducible by G, FINSEQ_3: 110;

              end;

                suppose

                 K: j <= i;

                1 <= (i + 1) & (i + 1) <= (lg1 + 1) by H1, XREAL_1: 6, NAT_1: 11;

                then (i + 1) in ( Seg (lg1 + 1));

                then

                reconsider ii = (i + 1) as Element of ( dom G) by LG1, FINSEQ_1:def 3;

                (G . ii) is irreducible by A3;

                hence (G1 . i) is irreducible by K, H1, LG1, FINSEQ_3: 111;

              end;

            end;

            then

             I2: G1 is_a_factorization_of ( Product G1);

            

             II: ( len G1) = k & ex p be Function of ( dom F1), ( dom G1) st p is bijective & for i be Element of ( dom F1) holds (G1 . (p . i)) is_associated_to (F1 . i) by IV, A4, A3, I0, I1, I2;

            thus

             III: ( len G) = (k + 1) by IV, A4, A3, I0, I1, I2, LG1;

            consider p be Function of ( dom F1), ( dom G1) such that

             P0: p is bijective & for i be Element of ( dom F1) holds (G1 . (p . i)) is_associated_to (F1 . i) by IV, A4, A3, I0, I1, I2;

            

             R0: p is one-to-one onto by P0;

            

             R1: ( rng p) = ( dom G1) by P0, FUNCT_2:def 3;

            defpred Q[ Nat, Nat] means ($2 = (p . $1) & (p . $1) < j & $1 <> (k + 1)) or ($2 = ((p . $1) + 1) & (p . $1) >= j & $1 <> (k + 1)) or ($2 = j & $1 = (k + 1));

            

             P1: for x be Element of ( dom F) holds ex y be Element of ( dom G) st Q[x, y]

            proof

              let x be Element of ( dom F);

              ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

              then

               Q0: 1 <= x & x <= (k + 1) by FINSEQ_1: 1;

              per cases ;

                suppose

                 Q1: x = (k + 1);

                take j;

                thus thesis by Q1;

              end;

                suppose

                 Q1: x <> (k + 1);

                then x < (k + 1) by Q0, XXREAL_0: 1;

                then x <= k by NAT_1: 13;

                then

                 Q2: x in ( Seg k) by Q0;

                ( dom F1) = ( Seg k) by A3, A4, FINSEQ_1:def 3;

                then

                 Q: (p . x) in ( dom G1) by Q2, R1, FUNCT_2: 4;

                then 1 <= (p . x) & (p . x) <= k by III, LG1, LG3, FINSEQ_1: 1;

                then 1 <= ((p . x) + 1) & ((p . x) + 1) <= (k + 1) by NAT_1: 11, XREAL_1: 6;

                then

                 R: ((p . x) + 1) in ( Seg (k + 1));

                now

                  per cases ;

                    suppose

                     Q3: (p . x) < j;

                    reconsider px = (p . x) as Element of ( dom G) by Q, LG2;

                    take px;

                    (px = (p . x) & (p . x) < j & x <> (k + 1)) by Q1, Q3;

                    hence thesis;

                  end;

                    suppose

                     Q3: (p . x) >= j;

                    reconsider px1 = ((p . x) + 1) as Element of ( dom G) by III, R, FINSEQ_1:def 3;

                    take px1;

                    px1 = ((p . x) + 1) & (p . x) >= j & x <> (k + 1) by Q1, Q3;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

            end;

            consider B be Function of ( dom F), ( dom G) such that

             P2: for x be Element of ( dom F) holds Q[x, (B . x)] from FUNCT_2:sch 3( P1);

            take B;

            now

              let x1,x2 be object;

              assume

               S0: x1 in ( dom F) & x2 in ( dom F) & (B . x1) = (B . x2);

              then

              reconsider x = x1, y = x2 as Element of ( dom F);

              

               S1: ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

              then

               S2: 1 <= x & x <= (k + 1) by FINSEQ_1: 1;

              

               S3: 1 <= y & y <= (k + 1) by S1, FINSEQ_1: 1;

              per cases ;

                suppose

                 S4: x = (k + 1);

                then

                 S5: j = (B . y) by S0, P2;

                now

                  assume

                   S6: y <> (k + 1);

                  per cases ;

                    suppose (p . y) < j;

                    hence contradiction by S5, S6, P2;

                  end;

                    suppose

                     S7: (p . y) >= j;

                    

                    then

                     S9: ((p . y) + 1) = (B . y) by S6, P2

                    .= j by S4, S0, P2;

                    consider k be Nat such that

                     S8: (p . y) = (j + k) by S7, NAT_1: 10;

                    (p . y) = (j - 1) by S9;

                    hence contradiction by S8;

                  end;

                end;

                hence x1 = x2 by S4;

              end;

                suppose

                 Q1: x <> (k + 1);

                then x < (k + 1) by S2, XXREAL_0: 1;

                then x <= k by NAT_1: 13;

                then

                 Q2: x in ( Seg k) by S2;

                

                 Q4: x in ( dom F1) by Q2, A3, A4, FINSEQ_1:def 3;

                 Q8:

                now

                  assume

                   R0: y = (k + 1);

                  then

                   R1: j = (B . x) by P2, S0;

                  (B . x) <> j

                  proof

                    per cases ;

                      suppose (p . x) < j;

                      hence thesis by Q1, P2;

                    end;

                      suppose

                       Q9: (p . x) >= j;

                      then

                       S9: ((p . x) + 1) = j by R1, Q1, P2;

                      consider k be Nat such that

                       S8: (p . x) = (j + k) by Q9, NAT_1: 10;

                      (p . x) = (j - 1) by S9;

                      hence thesis by S8;

                    end;

                  end;

                  hence contradiction by R0, S0, P2;

                end;

                then y < (k + 1) by S3, XXREAL_0: 1;

                then y <= k by NAT_1: 13;

                then

                 Q7: y in ( Seg k) by S3;

                ( dom F1) = ( Seg k) by A3, A4, FINSEQ_1:def 3;

                then

                 Q5: y in ( dom p) by Q7, FUNCT_2:def 1;

                

                 Q6: x in ( dom p) by Q4, FUNCT_2:def 1;

                now

                  per cases ;

                    suppose

                     Q3: (p . x) < j;

                    then

                     U1: (p . x) = (B . y) by S0, Q1, P2;

                    now

                      assume

                       U2: (p . y) >= j;

                      then ((p . y) + 1) = (p . x) by U1, Q8, P2;

                      then ((p . y) + 1) < (p . y) by Q3, U2, XXREAL_0: 2;

                      hence contradiction by NAT_1: 11;

                    end;

                    hence (p . x) = (p . y) by U1, Q8, P2;

                  end;

                    suppose

                     Q3: (p . x) >= j;

                    then

                     U1: ((p . x) + 1) = (B . y) by S0, Q1, P2;

                    now

                      assume

                       U2: (p . y) < j;

                      then (p . y) = ((p . x) + 1) by U1, Q8, P2;

                      then ((p . x) + 1) < (p . x) by U2, Q3, XXREAL_0: 2;

                      hence contradiction by NAT_1: 11;

                    end;

                    then ((p . y) + 1) = (B . y) by Q8, P2;

                    hence (p . x) = (p . y) by U1;

                  end;

                end;

                hence x1 = x2 by Q6, Q5, R0;

              end;

            end;

            then

             T: B is one-to-one by FUNCT_2: 19;

            now

              let x be object;

              now

                assume

                 U0: x in ( dom G);

                then

                 U1: x in ( Seg (k + 1)) by III, FINSEQ_1:def 3;

                

                 U2: ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

                then

                 U2a: ( dom F) = ( dom G) by III, FINSEQ_1:def 3;

                reconsider x1 = x as Element of ( dom F) by U2, U0, III, FINSEQ_1:def 3;

                

                 U3: 1 <= x1 & x1 <= (k + 1) by U1, FINSEQ_1: 1;

                

                 U8: ( dom B) = ( dom F) by FUNCT_2:def 1;

                ( dom p) = ( dom F1) by FUNCT_2:def 1;

                

                then

                 Q3: ( dom p) = ( Seg k) by A3, A4, FINSEQ_1:def 3

                .= ( dom G1) by II, FINSEQ_1:def 3;

                

                 Q4: ( Seg k) = ( dom G1) by II, FINSEQ_1:def 3;

                per cases ;

                  suppose

                   U7: x1 = j;

                  

                   U5: (k + 1) in ( dom B) by U8, U2, FINSEQ_1: 4;

                  then x1 = (B . (k + 1)) by U7, P2;

                  hence x in ( rng B) by U5, FUNCT_1:def 3;

                end;

                  suppose

                   Q1: x1 <> j;

                  now

                    per cases ;

                      suppose

                       QQ: x1 <= j;

                      then

                       QQQ: x1 < j by Q1, XXREAL_0: 1;

                      j <= (k + 1) by U2, FINSEQ_1: 1, U2a;

                      then x1 < (k + 1) by QQQ, XXREAL_0: 2;

                      then x1 <= k by NAT_1: 13;

                      then x1 in ( rng p) by U3, Q4, R1;

                      then

                      consider i be object such that

                       M: i in ( dom p) & (p . i) = x1 by FUNCT_1:def 3;

                      reconsider i as Element of ( dom p) by M;

                      i in ( dom G1) by Q3;

                      then i in ( Seg k) by II, FINSEQ_1:def 3;

                      then

                       H: 1 <= i & i <= k by FINSEQ_1: 1;

                      

                       N: (p . i) < j by M, QQ, Q1, XXREAL_0: 1;

                      k <= (k + 1) by NAT_1: 11;

                      then i <= (k + 1) by H, XXREAL_0: 2;

                      then i in ( Seg (k + 1)) by H;

                      then

                      reconsider i as Element of ( dom F) by A3, FINSEQ_1:def 3;

                      i <> (k + 1) by H, NAT_1: 19;

                      then (B . i) = x1 by M, N, P2;

                      hence x in ( rng B) by U8, FUNCT_1:def 3;

                    end;

                      suppose

                       QQ: x1 > j;

                      

                       QQ1: 1 <= j & j <= (k + 1) by U2, FINSEQ_1: 1, U2a;

                      

                       QQ2: (x1 - 1) <= ((k + 1) - 1) by U3, XREAL_1: 9;

                      1 < x1 by QQ, QQ1, XXREAL_0: 2;

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

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

                      then (x1 - 1) in ( rng p) by QQ2, Q4, R1, QQ;

                      then

                      consider i be object such that

                       M: i in ( dom p) & (p . i) = (x1 - 1) by FUNCT_1:def 3;

                      reconsider i as Element of ( dom p) by M;

                      i in ( dom G1) by Q3;

                      then i in ( Seg k) by II, FINSEQ_1:def 3;

                      then

                       H: 1 <= i & i <= k by FINSEQ_1: 1;

                      (j + 1) <= x1 by QQ, INT_1: 7;

                      then

                       N: ((j + 1) - 1) <= (x1 - 1) by XREAL_1: 9;

                      k <= (k + 1) by NAT_1: 11;

                      then i <= (k + 1) by H, XXREAL_0: 2;

                      then i in ( Seg (k + 1)) by H;

                      then

                      reconsider i as Element of ( dom F) by A3, FINSEQ_1:def 3;

                      i <> (k + 1) by H, NAT_1: 19;

                      

                      then (B . i) = ((p . i) + 1) by M, N, P2

                      .= x1 by M;

                      hence x in ( rng B) by U8, FUNCT_1:def 3;

                    end;

                  end;

                  hence x in ( rng B);

                end;

              end;

              hence x in ( dom G) iff x in ( rng B);

            end;

            then B is onto by TARSKI: 2, FUNCT_2:def 3;

            hence B is bijective by T;

            thus for i be Element of ( dom F) holds (G . (B . i)) is_associated_to (F . i)

            proof

              let i be Element of ( dom F);

              ( dom F) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

              then

               Q0: 1 <= i & i <= (k + 1) by FINSEQ_1: 1;

              per cases ;

                suppose i = (k + 1);

                hence thesis by P2, A6, E1;

              end;

                suppose

                 Q1: i <> (k + 1);

                then i < (k + 1) by Q0, XXREAL_0: 1;

                then i <= k by NAT_1: 13;

                then

                 Q2: i in ( Seg k) by Q0;

                i in ( dom F1) by Q2, A3, A4, FINSEQ_1:def 3;

                then (p . i) in ( dom G1) by R1, FUNCT_2: 4;

                then

                 V: 1 <= (p . i) & (p . i) <= k by III, LG1, LG3, FINSEQ_1: 1;

                reconsider if1 = i as Element of ( dom F1) by Q2, A3, A4, FINSEQ_1:def 3;

                now

                  per cases ;

                    suppose

                     Q3: (p . i) < j;

                    

                    then

                     S1: (G1 . (p . i)) = (G . (p . i)) by FINSEQ_3: 110

                    .= (G . (B . i)) by Q1, P2, Q3;

                    (F1 . if1) = (F . i) by B2, FINSEQ_1:def 7;

                    hence thesis by S1, P0;

                  end;

                    suppose

                     Q3: (p . i) >= j;

                    

                    then

                     S1: (G1 . (p . i)) = (G . ((p . i) + 1)) by V, III, FINSEQ_3: 111

                    .= (G . (B . i)) by Q1, Q3, P2;

                    (F1 . if1) = (F . i) by B2, FINSEQ_1:def 7;

                    hence thesis by S1, P0;

                  end;

                end;

                hence thesis;

              end;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 2( A0, A1);

      ex n be Nat st ( len F) = n;

      hence thesis by AS, I;

    end;

    registration

      let R be PIDomain;

      cluster factorizable -> uniquely_factorizable for Element of R;

      coherence

      proof

        let a be Element of R;

        assume

         AS: a is factorizable;

        hence a is factorizable;

        let F,G be Factorization of a;

        F is_a_factorization_of a & G is_a_factorization_of a by AS, ddf;

        hence thesis by lemfactunique;

      end;

    end

    definition

      let R be non degenerated Ring;

      :: RING_2:def15

      attr R is factorial means

      : df: for a be non zero Element of R st a is NonUnit of R holds a is uniquely_factorizable;

    end

    registration

      cluster factorial for non degenerated Ring;

      existence

      proof

        take the Field;

        thus thesis;

      end;

    end

    registration

      let R be factorial non degenerated Ring;

      cluster non zero non unital -> factorizable for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is non zero non unital;

        then a is uniquely_factorizable by df;

        hence thesis;

      end;

    end

    definition

      mode FactorialRing is factorial non degenerated Ring;

    end

    registration

      cluster PID -> factorial for domRing;

      coherence

      proof

        let R be domRing;

        assume

         Z: R is PID;

        assume R is non factorial;

        then

        consider a0 be non zero Element of R such that

         XX: a0 is NonUnit of R & not a0 is uniquely_factorizable;

        now

          assume

           X: not a0 is factorizable;

          ( {a0} -Ideal ) in ( Ideals R);

          then

          reconsider A = ( {a0} -Ideal ) as Element of ( Ideals R);

          defpred P[ set, set, set] means for a be Element of R holds (a <> ( 0. R) & a is non unital & not a is factorizable & $2 = ( {a} -Ideal )) implies (ex a1 be Element of R st a1 <> ( 0. R) & a1 is non unital & not a1 is factorizable & $3 = ( {a1} -Ideal ) & ( {a} -Ideal ) c= ( {a1} -Ideal ) & ( {a} -Ideal ) <> ( {a1} -Ideal ));

          

           A: for n be Nat holds for x be Element of ( Ideals R) holds ex y be Element of ( Ideals R) st P[n, x, y]

          proof

            let n be Nat, x be Element of ( Ideals R);

            

             A1: for a be Element of R holds (a <> ( 0. R) & a is non unital & not a is factorizable & x = ( {a} -Ideal )) implies (ex a1 be Element of R st a1 <> ( 0. R) & a1 is non unital & not a1 is factorizable & x c= ( {a1} -Ideal ) & x <> ( {a1} -Ideal ))

            proof

              let a be Element of R;

              assume

               A1: a <> ( 0. R) & a is non unital & not a is factorizable & x = ( {a} -Ideal );

              then a is reducible;

              then

              consider u be Element of R such that

               A3: u divides a & u is non unital & not u is_associated_to a by A1;

              consider s be Element of R such that

               A4: (u * s) = a by A3;

               A5:

              now

                assume u is factorizable & s is factorizable;

                then

                consider F,G be non empty FinSequence of R such that

                 H: F is_a_factorization_of u & G is_a_factorization_of s;

                (F ^ G) is_a_factorization_of a by A4, H, fact2;

                hence contradiction by A1;

              end;

              now

                per cases by A5;

                  suppose

                   B1: not s is factorizable;

                  

                   B2: s divides a by A4;

                  

                   B4: s <> ( 0. R) by A1, A4;

                  then

                   H: s is right_mult-cancelable by ALGSTR_0:def 37;

                   B3:

                  now

                    assume ( {a} -Ideal ) = ( {s} -Ideal );

                    then ex e be Element of R st e is unital & (s * e) = a by GCD_1: 18, div3;

                    hence contradiction by H, A4, A3;

                  end;

                  s is non unital by A4, A3, GCD_1: 18;

                  hence thesis by B1, B2, B3, B4, A1, div1;

                end;

                  suppose

                   B1: not u is factorizable;

                  

                   B3: ( {a} -Ideal ) <> ( {u} -Ideal ) by A3, div1;

                  u <> ( 0. R) by A4, A1;

                  hence thesis by B1, A3, div1, B3, A1;

                end;

              end;

              hence thesis;

            end;

            now

              per cases ;

                suppose

                 AA: ex a be Element of R st a <> ( 0. R) & a is non unital & not a is factorizable & x = ( {a} -Ideal );

                consider a1 be Element of R such that

                 A3: a1 <> ( 0. R) & a1 is non unital & not a1 is factorizable & x c= ( {a1} -Ideal ) & x <> ( {a1} -Ideal ) by A1, AA;

                ( {a1} -Ideal ) in ( Ideals R);

                then

                reconsider A1 = ( {a1} -Ideal ) as Element of ( Ideals R);

                 P[n, x, A1] by A3;

                hence ex Y be Element of ( Ideals R) st P[n, x, Y];

              end;

                suppose

                 AA: not ex a be Element of R st a <> ( 0. R) & a is non unital & not a is factorizable & x = ( {a} -Ideal );

                

                 A1: {( 0. R)} in ( Ideals R);

                 P[n, x, {( 0. R)}] by AA;

                hence ex y be Element of ( Ideals R) st P[n, x, y] by A1;

              end;

            end;

            hence ex y be Element of ( Ideals R) st P[n, x, y];

          end;

          ex f be sequence of ( Ideals R) st (f . 0 ) = A & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A);

          then

          consider F be sequence of ( Ideals R) such that

           C1: (F . 0 ) = A & for n be Nat holds P[n, (F . n), (F . (n + 1))];

          

           B: for i be Nat holds (F . i) c= (F . (i + 1)) & (F . i) <> (F . (i + 1))

          proof

            let i be Nat;

            defpred P[ Nat] means (ex a be Element of R st a <> ( 0. R) & a is non unital & not a is factorizable & (F . ($1 + 1)) = ( {a} -Ideal )) & (F . $1) c= (F . ($1 + 1)) & (F . $1) <> (F . ($1 + 1));

            

             A: P[ 0 ]

            proof

              

               A0: P[ 0 , (F . 0 ), (F . ( 0 + 1))] by C1;

              

               A3: ex a1 be Element of R st a1 <> ( 0. R) & a1 is non unital & not a1 is factorizable & (F . 1) = ( {a1} -Ideal ) & ( {a0} -Ideal ) c= ( {a1} -Ideal ) & ( {a0} -Ideal ) <> ( {a1} -Ideal ) by A0, C1, X, XX;

              thus ex a1 be Element of R st a1 <> ( 0. R) & a1 is non unital & not a1 is factorizable & (F . ( 0 + 1)) = ( {a1} -Ideal ) by A3;

              thus (F . 0 ) c= (F . ( 0 + 1)) & (F . 0 ) <> (F . ( 0 + 1)) by A3, C1;

            end;

            

             B: for k be Nat st P[k] holds P[(k + 1)]

            proof

              let k be Nat;

              assume P[k];

              then

              consider a be Element of R such that

               B1: a <> ( 0. R) & a is non unital & not a is factorizable & (F . (k + 1)) = ( {a} -Ideal ) & (F . k) c= (F . (k + 1)) & (F . k) <> (F . (k + 1));

              ex a1 be Element of R st a1 <> ( 0. R) & a1 is non unital & not a1 is factorizable & (F . ((k + 1) + 1)) = ( {a1} -Ideal ) & ( {a} -Ideal ) c= ( {a1} -Ideal ) & ( {a} -Ideal ) <> ( {a1} -Ideal ) by B1, C1;

              hence thesis by B1;

            end;

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

            hence thesis;

          end;

          then

          reconsider F as ascending Chain of ( Ideals R) by asc;

          now

            assume F is stagnating;

            then

            consider i be Nat such that

             D1: for j be Nat st j >= i holds (F . j) = (F . i);

            (F . (i + 1)) = (F . i) by D1, NAT_1: 11;

            hence contradiction by B;

          end;

          hence contradiction by Z;

        end;

        hence contradiction by Z, XX;

      end;

    end

    begin

    definition

      let L be Field;

      let p be Polynomial of L;

      :: RING_2:def16

      func deg* p -> Nat equals

      : S: ( deg p) if p <> ( 0_. L)

      otherwise 0 ;

      coherence

      proof

        per cases ;

          suppose p <> ( 0_. L);

          then p is non zero by UPROOTS:def 5;

          hence thesis by TARSKI: 1;

        end;

          suppose p = ( 0_. L);

          hence thesis;

        end;

      end;

      consistency ;

    end

    definition

      let L be Field;

      :: RING_2:def17

      func deg* L -> Function of ( Polynom-Ring L), NAT means

      : T: for p be Polynomial of L holds (it . p) = ( deg* p);

      existence

      proof

        set R = ( Polynom-Ring L);

        defpred P[ object, object] means ex p be Polynomial of L st $1 = p & $2 = ( deg* p);

        

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

        proof

          let x be object;

          assume x in the carrier of R;

          then

          reconsider p = x as Polynomial of L by POLYNOM3:def 10;

          take y = ( deg* p);

          thus thesis by ORDINAL1:def 12;

        end;

        ex f be Function of R, NAT st for x be object st x in the carrier of R holds P[x, (f . x)] from FUNCT_2:sch 1( A);

        then

        consider f be Function of ( Polynom-Ring L), NAT such that

         H: for x be object st x in the carrier of R holds P[x, (f . x)];

        take f;

        now

          let p be Polynomial of L;

          p in the carrier of R by POLYNOM3:def 10;

          then P[p, (f . p)] by H;

          hence (f . p) = ( deg* p);

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of ( Polynom-Ring L), NAT such that

         A1: for p be Polynomial of L holds (g1 . p) = ( deg* p) and

         A2: for p be Polynomial of L holds (g2 . p) = ( deg* p);

        

         A: ( dom g1) = the carrier of ( Polynom-Ring L) by FUNCT_2:def 1

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

        now

          let x be object;

          assume x in ( dom g1);

          then

          reconsider p = x as Polynomial of L by POLYNOM3:def 10;

          

          thus (g1 . x) = ( deg* p) by A1

          .= (g2 . x) by A2;

        end;

        hence thesis by A;

      end;

    end

    theorem :: RING_2:29

    

     degA: for L be Field holds for p be Polynomial of L holds for q be non zero Polynomial of L holds ( deg (p mod q)) < ( deg q)

    proof

      let L be Field;

      let p be Polynomial of L;

      let q be non zero Polynomial of L;

      set u = (p div q);

      q <> ( 0_. L);

      then

      consider r be Polynomial of L such that

       A: p = ((u *' q) + r) & ( deg r) < ( deg q) by HURWITZ:def 5;

      (p mod q) = (p - (u *' q)) by HURWITZ:def 6

      .= (((u *' q) + r) + ( - (u *' q))) by A, POLYNOM3:def 6

      .= (((u *' q) + ( - (u *' q))) + r) by POLYNOM3: 26

      .= (((u *' q) - (u *' q)) + r) by POLYNOM3:def 6

      .= (( 0_. L) + r) by POLYNOM3: 29

      .= r by POLYNOM3: 28;

      hence thesis by A;

    end;

    theorem :: RING_2:30

    

     thEucl1: for L be Field, p be Element of ( Polynom-Ring L), q be non zero Element of ( Polynom-Ring L) holds ex u,r be Element of ( Polynom-Ring L) st p = ((u * q) + r) & (r = ( 0. ( Polynom-Ring L)) or (( deg* L) . r) < (( deg* L) . q))

    proof

      let L be Field, p be Element of ( Polynom-Ring L), q be non zero Element of ( Polynom-Ring L);

      q <> ( 0. ( Polynom-Ring L));

      then

       AS: q <> ( 0_. L) by POLYNOM3:def 10;

      then

      reconsider q1 = q as non zero Polynomial of L by UPROOTS:def 5, POLYNOM3:def 10;

      reconsider p1 = p as Polynomial of L by POLYNOM3:def 10;

      set u = (p1 div q1), r = (p1 mod q1);

      reconsider u, r as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      take u, r;

      

       A: (((p1 div q1) *' q1) + (p1 mod q1)) = (((p1 div q1) *' q1) + (p1 - ((p1 div q1) *' q1))) by HURWITZ:def 6

      .= (((p1 div q1) *' q1) + (p1 + ( - ((p1 div q1) *' q1)))) by POLYNOM3:def 6

      .= ((((p1 div q1) *' q1) + ( - ((p1 div q1) *' q1))) + p1) by POLYNOM3: 26

      .= ((((p1 div q1) *' q1) - ((p1 div q1) *' q1)) + p1) by POLYNOM3:def 6

      .= (( 0_. L) + p1) by POLYNOM3: 29

      .= p1 by POLYNOM3: 28;

      ((p1 div q1) *' q1) = (u * q) by POLYNOM3:def 10;

      hence p = ((u * q) + r) by A, POLYNOM3:def 10;

      now

        assume r <> ( 0. ( Polynom-Ring L));

        then

         C: (p1 mod q1) <> ( 0_. L) by POLYNOM3:def 10;

        

         B: (( deg* L) . r) = ( deg* (p1 mod q1)) by T

        .= ( deg (p1 mod q1)) by C, S;

        (( deg* L) . q) = ( deg* q1) by T

        .= ( deg q1) by AS, S;

        hence (( deg* L) . r) < (( deg* L) . q) by B, degA;

      end;

      hence thesis;

    end;

    

     thEucl2: for L be Field holds ex f be Function of ( Polynom-Ring L), NAT st for p,q be Element of ( Polynom-Ring L) st q <> ( 0. ( Polynom-Ring L)) holds ex u,r be Element of ( Polynom-Ring L) st p = ((u * q) + r) & (r = ( 0. ( Polynom-Ring L)) or (f . r) < (f . q))

    proof

      let L be Field;

      take f = ( deg* L);

      now

        let p,q be Element of ( Polynom-Ring L);

        assume q <> ( 0. ( Polynom-Ring L));

        then q is non zero;

        hence ex u,r be Element of ( Polynom-Ring L) st p = ((u * q) + r) & (r = ( 0. ( Polynom-Ring L)) or (f . r) < (f . q)) by thEucl1;

      end;

      hence thesis;

    end;

    registration

      let L be Field;

      cluster ( Polynom-Ring L) -> Euclidian;

      coherence

      proof

        ex f be Function of ( Polynom-Ring L), NAT st for a,b be Element of ( Polynom-Ring L) st b <> ( 0. ( Polynom-Ring L)) holds ex q,r be Element of ( Polynom-Ring L) st a = ((q * b) + r) & (r = ( 0. ( Polynom-Ring L)) or (f . r) < (f . b)) by thEucl2;

        hence thesis by INT_3:def 8;

      end;

    end

    definition

      let L be Field;

      :: original: deg*

      redefine

      func deg* L -> DegreeFunction of ( Polynom-Ring L) ;

      coherence

      proof

        let a,b be Element of ( Polynom-Ring L);

        assume b <> ( 0. ( Polynom-Ring L));

        then b is non zero;

        hence thesis by thEucl1;

      end;

    end