ideal_1.miz

    begin

    registration

      cluster add-associative left_zeroed right_zeroed for non empty addLoopStr;

      existence

      proof

        set R = the non degenerated comRing;

        take R;

        thus thesis;

      end;

    end

    registration

      cluster Abelian left_zeroed right_zeroed add-cancelable well-unital add-associative associative commutative distributive for non trivial doubleLoopStr;

      existence

      proof

        set R = the non degenerated comRing;

        take R;

        thus thesis;

      end;

    end

    theorem :: IDEAL_1:1



     Th1: for V be add-associative left_zeroed right_zeroed non empty addLoopStr, v,u be Element of V holds ( Sum <*v, u*>) = (v + u)

    proof

      let V be add-associative left_zeroed right_zeroed non empty addLoopStr, v,u be Element of V;

       <*v, u*> = ( <*v*> ^ <*u*>) by FINSEQ_1:def 9;



      then ( Sum <*v, u*>) = (( Sum <*v*>) + ( Sum <*u*>)) by RLVECT_1: 41

      .= (v + ( Sum <*u*>)) by BINOM: 3

      .= (v + u) by BINOM: 3;

      hence thesis;

    end;

    begin

    definition

      let L be non empty addLoopStr, F be Subset of L;

      :: IDEAL_1:def1

      attr F is add-closed means

      : Def1: for x,y be Element of L st x in F & y in F holds (x + y) in F;

    end

    definition

      let L be non empty multMagma, F be Subset of L;

      :: IDEAL_1:def2

      attr F is left-ideal means

      : Def2: for p,x be Element of L st x in F holds (p * x) in F;

      :: IDEAL_1:def3

      attr F is right-ideal means

      : Def3: for p,x be Element of L st x in F holds (x * p) in F;

    end

    registration

      let L be non empty addLoopStr;

      cluster add-closed for non empty Subset of L;

      existence

      proof

        set M = the carrier of L;

        for u be object holds u in M implies u in the carrier of L;

        then

        reconsider M as Subset of L by TARSKI:def 3;

        reconsider M as non empty Subset of L;

        take M;

        thus thesis;

      end;

    end

    registration

      let L be non empty multMagma;

      cluster left-ideal for non empty Subset of L;

      existence

      proof

        set M = the carrier of L;

        for u be object holds u in M implies u in the carrier of L;

        then

        reconsider M as Subset of L by TARSKI:def 3;

        reconsider M as non empty Subset of L;

        take M;

        thus thesis;

      end;

      cluster right-ideal for non empty Subset of L;

      existence

      proof

        set M = the carrier of L;

        for u be object holds u in M implies u in the carrier of L;

        then

        reconsider M as Subset of L by TARSKI:def 3;

        reconsider M as non empty Subset of L;

        take M;

        thus thesis;

      end;

    end

    registration

      let L be non empty doubleLoopStr;

      cluster add-closed left-ideal right-ideal for non empty Subset of L;

      existence

      proof

        set M = the carrier of L;

        for u be object holds u in M implies u in the carrier of L;

        then

        reconsider M as Subset of L by TARSKI:def 3;

        reconsider M as non empty Subset of L;

        take M;

        thus thesis;

      end;

      cluster add-closed right-ideal for non empty Subset of L;

      existence

      proof

        set M = the carrier of L;

        for u be object holds u in M implies u in the carrier of L;

        then

        reconsider M as Subset of L by TARSKI:def 3;

        reconsider M as non empty Subset of L;

        take M;

        thus thesis;

      end;

      cluster add-closed left-ideal for non empty Subset of L;

      existence

      proof

        set M = the carrier of L;

        for u be object holds u in M implies u in the carrier of L;

        then

        reconsider M as Subset of L by TARSKI:def 3;

        reconsider M as non empty Subset of L;

        take M;

        thus thesis;

      end;

    end

    registration

      let R be commutative non empty multMagma;

      cluster left-ideal -> right-ideal for non empty Subset of R;

      coherence

      proof

        let I be non empty Subset of R;

        assume I is left-ideal;

        then for p,x be Element of R st x in I holds (x * p) in I;

        hence thesis;

      end;

      cluster right-ideal -> left-ideal for non empty Subset of R;

      coherence

      proof

        let I be non empty Subset of R;

        assume I is right-ideal;

        then for p,x be Element of R st x in I holds (p * x) in I;

        hence thesis;

      end;

    end

    definition

      let L be non empty doubleLoopStr;

      mode Ideal of L is add-closed left-ideal right-ideal non empty Subset of L;

    end

    definition

      let L be non empty doubleLoopStr;

      mode RightIdeal of L is add-closed right-ideal non empty Subset of L;

    end

    definition

      let L be non empty doubleLoopStr;

      mode LeftIdeal of L is add-closed left-ideal non empty Subset of L;

    end

    theorem :: IDEAL_1:2



     Th2: for R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be left-ideal non empty Subset of R holds ( 0. R) in I

    proof

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr;

      let I be left-ideal non empty Subset of R;

      set a = the Element of I;

      (( 0. R) * a) in I by Def2;

      hence thesis by BINOM: 1;

    end;

    theorem :: IDEAL_1:3



     Th3: for R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R holds ( 0. R) in I

    proof

      let R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr;

      let I be right-ideal non empty Subset of R;

      set a = the Element of I;

      (a * ( 0. R)) in I by Def3;

      hence thesis by BINOM: 2;

    end;

    theorem :: IDEAL_1:4



     Th4: for L be right_zeroed non empty addLoopStr holds {( 0. L)} is add-closed

    proof

      let L be right_zeroed non empty addLoopStr;

      let x,y be Element of L;

      assume x in {( 0. L)} & y in {( 0. L)};

      then x = ( 0. L) & y = ( 0. L) by TARSKI:def 1;

      then (x + y) = ( 0. L) by RLVECT_1:def 4;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: IDEAL_1:5



     Th5: for L be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr holds {( 0. L)} is left-ideal

    proof

      let L be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr;

      let p,x be Element of L;

      reconsider p9 = p as Element of L;

      assume x in {( 0. L)};

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

      then (p9 * x) = ( 0. L) by BINOM: 2;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: IDEAL_1:6



     Th6: for L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr holds {( 0. L)} is right-ideal

    proof

      let L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr;

      let p,x be Element of L;

      reconsider p9 = p as Element of L;

      assume x in {( 0. L)};

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

      then (x * p9) = ( 0. L) by BINOM: 1;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let L be right_zeroed non empty addLoopStr;

      cluster {( 0. L)} -> add-closed;

      coherence by Th4;

    end

    registration

      let L be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr;

      cluster {( 0. L)} -> left-ideal;

      coherence by Th5;

    end

    registration

      let L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr;

      cluster {( 0. L)} -> right-ideal;

      coherence by Th6;

    end

    theorem :: IDEAL_1:7

    for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds {( 0. L)} is Ideal of L;

    theorem :: IDEAL_1:8

    for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds {( 0. L)} is LeftIdeal of L;

    theorem :: IDEAL_1:9

    for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds {( 0. L)} is RightIdeal of L;

    theorem :: IDEAL_1:10



     Th10: for L be non empty doubleLoopStr holds the carrier of L is Ideal of L

    proof

      let L be non empty doubleLoopStr;

      the carrier of L c= the carrier of L;

      then

      reconsider cL = the carrier of L as Subset of L;



       A1: cL is left-ideal;



       A2: cL is right-ideal;

      cL is add-closed;

      hence thesis by A1, A2;

    end;

    theorem :: IDEAL_1:11



     Th11: for L be non empty doubleLoopStr holds the carrier of L is LeftIdeal of L

    proof

      let L be non empty doubleLoopStr;

      the carrier of L c= the carrier of L;

      then

      reconsider cL = the carrier of L as Subset of L;



       A1: cL is left-ideal;

      cL is add-closed;

      hence thesis by A1;

    end;

    theorem :: IDEAL_1:12



     Th12: for L be non empty doubleLoopStr holds the carrier of L is RightIdeal of L

    proof

      let L be non empty doubleLoopStr;

      the carrier of L c= the carrier of L;

      then

      reconsider cL = the carrier of L as Subset of L;



       A1: cL is right-ideal;

      cL is add-closed;

      hence thesis by A1;

    end;

    definition

      let R be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr, I be Ideal of R;

      :: original: trivial

      redefine

      :: IDEAL_1:def4

      attr I is trivial means I = {( 0. R)};

      compatibility

      proof

        now

          assume I is trivial;

          then

          consider x be object such that

           A1: I = {x} by ZFMISC_1: 131;

          ( 0. R) in {x} by A1, Th3;

          hence I = {( 0. R)} by A1, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non trivial left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr;

      cluster proper for Ideal of R;

      existence

      proof

        reconsider M = {( 0. R)} as Ideal of R;

        M is proper by SUBSET_1:def 6;

        hence thesis;

      end;

    end

    theorem :: IDEAL_1:13



     Th13: for L be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr, I be left-ideal non empty Subset of L, x be Element of L st x in I holds ( - x) in I

    proof

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

      let I be left-ideal non empty Subset of L;

      let x be Element of L;

      assume x in I;

      then

       A1: (( - ( 1. L)) * x) in I by Def2;

      ( 0. L) = (( 0. L) * x)

      .= ((( 1. L) + ( - ( 1. L))) * x) by RLVECT_1:def 10

      .= ((( 1. L) * x) + (( - ( 1. L)) * x)) by VECTSP_1:def 3

      .= (x + (( - ( 1. L)) * x));

      hence thesis by A1, RLVECT_1:def 10;

    end;

    theorem :: IDEAL_1:14



     Th14: for L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr, I be right-ideal non empty Subset of L, x be Element of L st x in I holds ( - x) in I

    proof

      let L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr;

      let I be right-ideal non empty Subset of L;

      let x be Element of L;

      assume x in I;

      then

       A1: (x * ( - ( 1. L))) in I by Def3;

      ( 0. L) = (x * ( 0. L))

      .= (x * (( 1. L) + ( - ( 1. L)))) by RLVECT_1:def 10

      .= ((x * ( 1. L)) + (x * ( - ( 1. L)))) by VECTSP_1:def 2

      .= (x + (x * ( - ( 1. L))));

      hence thesis by A1, RLVECT_1:def 10;

    end;

    theorem :: IDEAL_1:15

    for L be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr, I be LeftIdeal of L, x,y be Element of L st x in I & y in I holds (x - y) in I

    proof

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

      let I be LeftIdeal of L;

      let x,y be Element of L;

      assume that

       A1: x in I and

       A2: y in I;

      ( - y) in I by A2, Th13;

      hence thesis by A1, Def1;

    end;

    theorem :: IDEAL_1:16

    for L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr, I be RightIdeal of L, x,y be Element of L st x in I & y in I holds (x - y) in I

    proof

      let L be add-associative right_zeroed right_complementable right-distributive right_unital non empty doubleLoopStr;

      let I be RightIdeal of L;

      let x,y be Element of L;

      assume that

       A1: x in I and

       A2: y in I;

      ( - y) in I by A2, Th14;

      hence thesis by A1, Def1;

    end;

    theorem :: IDEAL_1:17



     Th17: for R be left_zeroed right_zeroed add-cancelable add-associative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, a be Element of I, n be Element of NAT holds (n * a) in I

    proof

      let R be left_zeroed right_zeroed add-cancelable add-associative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, a be Element of I, n be Element of NAT ;

      defpred P[ Nat] means ($1 * a) in I;



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

      proof

        let n be Nat;



         A2: ((n + 1) * a) = ((1 * a) + (n * a)) by BINOM: 15

        .= (a + (n * a)) by BINOM: 13;

        assume (n * a) in I;

        hence thesis by A2, Def1;

      end;

      ( 0 * a) = ( 0. R) by BINOM: 12;

      then

       A3: P[ 0 ] by Th3;

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: IDEAL_1:18

    for R be well-unital left_zeroed right_zeroed add-cancelable associative distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R, a be Element of I, n be Element of NAT st n <> 0 holds (a |^ n) in I

    proof

      let R be well-unital left_zeroed right_zeroed add-cancelable associative distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R, a be Element of I, n be Element of NAT ;

      defpred P[ Nat] means (a |^ $1) in I;

      assume

       A1: n <> 0 ;



       A2: for n be Nat st 1 <= n holds P[n] implies P[(n + 1)]

      proof

        let n be Nat;

        assume 1 <= n;



         A3: (a |^ (n + 1)) = ((a |^ n) * (a |^ 1)) by BINOM: 10;

        assume (a |^ n) in I;

        hence thesis by A3, Def3;

      end;

      (a |^ 1) = a by BINOM: 8;

      then

       A4: P[1];

      for n be Nat st 1 <= n holds P[n] from NAT_1:sch 8( A4, A2);

      hence thesis by A1, NAT_1: 14;

    end;

    definition

      let R be non empty addLoopStr, I be add-closed non empty Subset of R;

      :: IDEAL_1:def5

      func add| (I,R) -> BinOp of I equals (the addF of R || I);

      coherence

      proof

        reconsider f = (the addF of R || I) as Function of [:I, I:], the carrier of R by FUNCT_2: 32;



         A1: ( dom f) = [:I, I:] by FUNCT_2:def 1;

        for x be object st x in [:I, I:] holds (f . x) in I

        proof

          let x be object;

          assume

           A2: x in [:I, I:];

          then

          consider u,v be object such that

           A3: u in I & v in I and

           A4: x = [u, v] by ZFMISC_1:def 2;

          reconsider u, v as Element of R by A3;

          reconsider u, v as Element of R;

          (f . x) = (u + v) by A1, A2, A4, FUNCT_1: 47;

          hence thesis by A3, Def1;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let R be non empty multMagma, I be right-ideal non empty Subset of R;

      :: IDEAL_1:def6

      func mult| (I,R) -> BinOp of I equals (the multF of R || I);

      coherence

      proof

        reconsider f = (the multF of R || I) as Function of [:I, I:], the carrier of R by FUNCT_2: 32;



         A1: ( dom f) = [:I, I:] by FUNCT_2:def 1;

        for x be object st x in [:I, I:] holds (f . x) in I

        proof

          let x be object;

          assume x in [:I, I:];

          then

          consider u,v be object such that

           A2: u in I & v in I and

           A3: x = [u, v] by ZFMISC_1:def 2;

          reconsider u, v as Element of I by A2;

          (f . x) = (the multF of R . [u, v]) by A1, A3, FUNCT_1: 47

          .= (u * v);

          hence thesis by Def3;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let R be non empty addLoopStr, I be add-closed non empty Subset of R;

      :: IDEAL_1:def7

      func Gr (I,R) -> non empty addLoopStr equals addLoopStr (# I, ( add| (I,R)), ( In (( 0. R),I)) #);

      coherence ;

    end

    registration

      let R be left_zeroed right_zeroed add-cancelable add-associative distributive non empty doubleLoopStr, I be add-closed non empty Subset of R;

      cluster ( Gr (I,R)) -> add-associative;

      coherence

      proof

        set M = addLoopStr (# I, ( add| (I,R)), ( In (( 0. R),I)) #);

        reconsider M as non empty addLoopStr;

        now

          let u be object;



           A1: ( dom the addF of R) = [:the carrier of R, the carrier of R:] by FUNCT_2:def 1;

          assume u in [:I, I:];

          hence u in ( dom the addF of R) by A1;

        end;

        then [:I, I:] c= ( dom the addF of R);

        then

         A2: ( dom (the addF of R || I)) = [:I, I:] by RELAT_1: 62;



         A3: for a,b be Element of M, a9,b9 be Element of I st a9 = a & b9 = b holds (a + b) = (a9 + b9)

        proof

          let a,b be Element of M, a9,b9 be Element of I;

          assume

           A4: a9 = a & b9 = b;

           [a9, b9] in ( dom (the addF of R || I)) by A2;

          hence thesis by A4, FUNCT_1: 47;

        end;

        now

          let a,b,c be Element of M;

          reconsider a9 = a, b9 = b, c9 = c as Element of I;

          (a9 + b9) in I by Def1;

          then

           A5: [(a9 + b9), c9] in ( dom (the addF of R || I)) by A2, ZFMISC_1:def 2;

          (b9 + c9) in I by Def1;

          then

           A6: [a9, (b9 + c9)] in ( dom (the addF of R || I)) by A2, ZFMISC_1:def 2;



          thus ((a + b) + c) = ((the addF of R || I) . [(a9 + b9), c9]) by A3

          .= ((a9 + b9) + c9) by A5, FUNCT_1: 47

          .= (a9 + (b9 + c9)) by RLVECT_1:def 3

          .= (( add| (I,R)) . [a9, (b9 + c9)]) by A6, FUNCT_1: 47

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

        end;

        hence thesis by RLVECT_1:def 3;

      end;

    end

    registration

      let R be left_zeroed right_zeroed add-cancelable add-associative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R;

      cluster ( Gr (I,R)) -> right_zeroed;

      coherence

      proof

        set M = addLoopStr (# I, ( add| (I,R)), ( In (( 0. R),I)) #);

        reconsider M as non empty addLoopStr;

        now

          let u be object;



           A1: ( dom the addF of R) = [:the carrier of R, the carrier of R:] by FUNCT_2:def 1;

          assume u in [:I, I:];

          hence u in ( dom the addF of R) by A1;

        end;

        then [:I, I:] c= ( dom the addF of R);

        then

         A2: ( dom (the addF of R || I)) = [:I, I:] by RELAT_1: 62;

        now

          let a be Element of M;

          reconsider a9 = a as Element of I;

          ( 0. R) in I by Th3;

          then

           A3: [a9, ( 0. R)] in ( dom (the addF of R || I)) by A2, ZFMISC_1:def 2;



          thus (a + ( 0. M)) = ((the addF of R || I) . [a9, ( 0. R)]) by Th3, SUBSET_1:def 8

          .= (a9 + ( 0. R)) by A3, FUNCT_1: 47

          .= a by RLVECT_1:def 4;

        end;

        hence thesis by RLVECT_1:def 4;

      end;

    end

    registration

      let R be Abelian non empty doubleLoopStr, I be add-closed non empty Subset of R;

      cluster ( Gr (I,R)) -> Abelian;

      coherence

      proof

        set M = addLoopStr (# I, ( add| (I,R)), ( In (( 0. R),I)) #);

        reconsider M as non empty addLoopStr;

        now

          let u be object;



           A1: ( dom the addF of R) = [:the carrier of R, the carrier of R:] by FUNCT_2:def 1;

          assume u in [:I, I:];

          hence u in ( dom the addF of R) by A1;

        end;

        then [:I, I:] c= ( dom the addF of R);

        then

         A2: ( dom (the addF of R || I)) = [:I, I:] by RELAT_1: 62;



         A3: for a,b be Element of M, a9,b9 be Element of I st a9 = a & b9 = b holds (a + b) = (a9 + b9)

        proof

          let a,b be Element of M, a9,b9 be Element of I;

          assume

           A4: a9 = a & b9 = b;

           [a9, b9] in ( dom (the addF of R || I)) by A2;

          hence thesis by A4, FUNCT_1: 47;

        end;

        now

          let a,b be Element of M;

          reconsider a9 = a, b9 = b as Element of I;



          thus (a + b) = (a9 + b9) by A3

          .= (b + a) by A3;

        end;

        hence thesis by RLVECT_1:def 2;

      end;

    end

    registration

      let R be Abelian right_unital left_zeroed right_zeroed right_complementable add-associative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R;

      cluster ( Gr (I,R)) -> right_complementable;

      coherence

      proof

        set M = addLoopStr (# I, ( add| (I,R)), ( In (( 0. R),I)) #);

        reconsider M as non empty addLoopStr;

        now

          let u be object;



           A1: ( dom the addF of R) = [:the carrier of R, the carrier of R:] by FUNCT_2:def 1;

          assume u in [:I, I:];

          hence u in ( dom the addF of R) by A1;

        end;

        then [:I, I:] c= ( dom the addF of R);

        then

         A2: ( dom (the addF of R || I)) = [:I, I:] by RELAT_1: 62;



         A3: for a,b be Element of M, a9,b9 be Element of I st a9 = a & b9 = b holds (a + b) = (a9 + b9)

        proof

          let a,b be Element of M, a9,b9 be Element of I;

          assume

           A4: a9 = a & b9 = b;

           [a9, b9] in ( dom (the addF of R || I)) by A2;

          hence thesis by A4, FUNCT_1: 47;

        end;

        reconsider I as RightIdeal of R;

        M is right_complementable

        proof

          let a be Element of M;

          reconsider a9 = a as Element of I;

          reconsider b = ( - a9) as Element of M by Th14;

          (a + b) = (a9 + ( - a9)) by A3

          .= ( 0. R) by RLVECT_1: 5

          .= ( 0. M) by Th3, SUBSET_1:def 8;

          hence ex b be Element of M st (a + b) = ( 0. M);

        end;

        hence thesis;

      end;

    end



     Lm1: for R be comRing, a be Element of R holds the set of all (a * r) where r be Element of R is Ideal of R

    proof

      let R be comRing, a be Element of R;

      set M = the set of all (a * r) where r be Element of R;

       A1:

      now

        let u be object;

        assume u in M;

        then ex r be Element of R st u = (a * r);

        hence u in the carrier of R;

      end;

      (a * ( 1. R)) in M;

      then

      reconsider M as non empty Subset of R by A1, TARSKI:def 3;

      reconsider M as non empty Subset of R;

       A2:

      now

        let b,c be Element of R;

        assume that

         A3: b in M and

         A4: c in M;

        consider r be Element of R such that

         A5: (a * r) = b by A3;

        consider s be Element of R such that

         A6: (a * s) = c by A4;

        (b + c) = (a * (r + s)) by A5, A6, VECTSP_1:def 7;

        hence (b + c) in M;

      end;

       A7:

      now

        let s,b be Element of R;

        assume b in M;

        then

        consider r be Element of R such that

         A8: (a * r) = b;

        (s * b) = ((s * r) * a) by A8, GROUP_1:def 3;

        hence (s * b) in M;

      end;

      now

        let s,b be Element of R;

        assume b in M;

        then

        consider r be Element of R such that

         A9: (a * r) = b;

        (b * s) = (a * (r * s)) by A9, GROUP_1:def 3;

        hence (b * s) in M;

      end;

      hence thesis by A2, A7, Def1, Def2, Def3;

    end;

    theorem :: IDEAL_1:19



     Th19: for R be right_unital non empty doubleLoopStr, I be left-ideal non empty Subset of R holds I is proper iff not (( 1. R) in I)

    proof

      let R be right_unital non empty doubleLoopStr, I be left-ideal non empty Subset of R;

       A1:

      now

        assume

         A2: I is proper;

        thus not ( 1. R) in I

        proof

          assume

           A3: ( 1. R) in I;

           A4:

          now

            let u be object;

            assume u in the carrier of R;

            then

            reconsider u9 = u as Element of R;

            (u9 * ( 1. R)) = u9;

            hence u in I by A3, Def2;

          end;

          for u be object holds u in I implies u in the carrier of R;

          then I = the carrier of R by A4, TARSKI: 2;

          hence thesis by A2, SUBSET_1:def 6;

        end;

      end;

      now

        assume not ( 1. R) in I;

        then I <> the carrier of R;

        hence I is proper by SUBSET_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: IDEAL_1:20

    for R be left_unital right_unital non empty doubleLoopStr, I be right-ideal non empty Subset of R holds I is proper iff for u be Element of R st u is unital holds not (u in I)

    proof

      let R be left_unital right_unital non empty doubleLoopStr, I be right-ideal non empty Subset of R;

       A1:

      now

        assume

         A2: I is proper;



         A3: not ( 1. R) in I

        proof

          assume

           A4: ( 1. R) in I;

           A5:

          now

            let u be object;

            assume u in the carrier of R;

            then

            reconsider u9 = u as Element of R;

            (( 1. R) * u9) = u9;

            hence u in I by A4, Def3;

          end;

          for u be object holds u in I implies u in the carrier of R;

          then I = the carrier of R by A5, TARSKI: 2;

          hence thesis by A2, SUBSET_1:def 6;

        end;

        thus for u be Element of R st u is unital holds not u in I

        proof

          let u be Element of R;

          assume u is unital;

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

          then ex b be Element of R st ( 1. R) = (u * b) by GCD_1:def 1;

          hence thesis by A3, Def3;

        end;

      end;

      now

        ( 1. R) divides ( 1. R);

        then

         A6: ( 1. R) is unital by GCD_1:def 2;

        assume for u be Element of R st u is unital holds not u in I;

        then I <> the carrier of R by A6;

        hence I is proper by SUBSET_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: IDEAL_1:21

    for R be right_unital non empty doubleLoopStr, I be left-ideal right-ideal non empty Subset of R holds I is proper iff for u be Element of R st u is unital holds not (u in I)

    proof

      let R be right_unital non empty doubleLoopStr, I be left-ideal right-ideal non empty Subset of R;

       A1:

      now

        assume

         A2: I is proper;



         A3: not ( 1. R) in I

        proof

          assume

           A4: ( 1. R) in I;

           A5:

          now

            let u be object;

            assume u in the carrier of R;

            then

            reconsider u9 = u as Element of R;

            (u9 * ( 1. R)) = u9;

            hence u in I by A4, Def2;

          end;

          for u be object holds u in I implies u in the carrier of R;

          then I = the carrier of R by A5, TARSKI: 2;

          hence thesis by A2, SUBSET_1:def 6;

        end;

        thus for u be Element of R st u is unital holds not u in I

        proof

          let u be Element of R;

          assume u is unital;

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

          then ex b be Element of R st ( 1. R) = (u * b) by GCD_1:def 1;

          hence thesis by A3, Def3;

        end;

      end;

      now

        ( 1. R) divides ( 1. R);

        then

         A6: ( 1. R) is unital by GCD_1:def 2;

        assume for u be Element of R st u is unital holds not u in I;

        then I <> the carrier of R by A6;

        hence I is proper by SUBSET_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: IDEAL_1:22

    for R be non degenerated comRing holds R is Field iff for I be Ideal of R holds (I = {( 0. R)} or I = the carrier of R)

    proof

      let R be non degenerated comRing;

       A1:

      now

        assume

         A2: R is Field;

        thus for I be Ideal of R holds (I = {( 0. R)} or I = the carrier of R)

        proof

          let I be Ideal of R;

          assume

           A3: I <> {( 0. R)};

          reconsider R as Field by A2;

          ex a be Element of R st a in I & a <> ( 0. R)

          proof

            assume

             A4: not (ex a be Element of R st a in I & a <> ( 0. R));

             A5:

            now

              let u be object;

              assume u in I;

              then

              reconsider u9 = u as Element of I;

              u9 = ( 0. R) by A4;

              hence u in {( 0. R)} by TARSKI:def 1;

            end;

            now

              let u be object;

              assume

               A6: u in {( 0. R)};

              then

              reconsider u9 = u as Element of R;

              u9 = ( 0. R) by A6, TARSKI:def 1;

              hence u in I by Th3;

            end;

            hence thesis by A3, A5, TARSKI: 2;

          end;

          then

          consider a be Element of R such that

           A7: a in I and

           A8: a <> ( 0. R);

          ex b be Element of R st (b * a) = ( 1. R) by A8, VECTSP_1:def 9;

          then ( 1. R) in I by A7, Def3;

          then I is non proper by Th19;

          hence thesis by SUBSET_1:def 6;

        end;

      end;

      now

        assume

         A9: for I be Ideal of R holds (I = {( 0. R)} or I = the carrier of R);

        now

          let a be Element of R;

          reconsider a9 = a as Element of R;

          reconsider M = the set of all (a9 * r) where r be Element of R as Ideal of R by Lm1;

          (a * ( 1. R)) = a;

          then

           A10: a in M;

          assume a <> ( 0. R);

          then M <> {( 0. R)} by A10, TARSKI:def 1;

          then M = the carrier of R by A9;

          then ( 1. R) in M;

          then ex b be Element of R st (a * b) = ( 1. R);

          hence ex b be Element of R st (b * a) = ( 1. R);

        end;

        hence R is Field by VECTSP_1:def 9;

      end;

      hence thesis by A1;

    end;

    begin

    definition

      let R be non empty multLoopStr, A be non empty Subset of R;

      :: IDEAL_1:def8

      mode LinearCombination of A -> FinSequence of the carrier of R means

      : Def8: for i be set st i in ( dom it ) holds ex u,v be Element of R, a be Element of A st (it /. i) = ((u * a) * v);

      existence

      proof

        set p = ( <*> the carrier of R);

        take p;

        let i be set;

        thus thesis;

      end;

      :: IDEAL_1:def9

      mode LeftLinearCombination of A -> FinSequence of the carrier of R means

      : Def9: for i be set st i in ( dom it ) holds ex u be Element of R, a be Element of A st (it /. i) = (u * a);

      existence

      proof

        set a = the Element of A;

        reconsider aR = a as Element of R;

        reconsider a9 = (a * a) as Element of R;

        set p = <*a9*>;

        take p;

        let i be set;

        assume

         A1: i in ( dom p);

        take aR, a;

        ( dom p) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A2: i = 1 by A1, TARSKI:def 1;



        thus (p /. i) = (p . i) by A1, PARTFUN1:def 6

        .= (aR * a) by A2, FINSEQ_1: 40;

      end;

      :: IDEAL_1:def10

      mode RightLinearCombination of A -> FinSequence of the carrier of R means

      : Def10: for i be set st i in ( dom it ) holds ex u be Element of R, a be Element of A st (it /. i) = (a * u);

      existence

      proof

        set a = the Element of A;

        reconsider aR = a as Element of R;

        reconsider a9 = (a * a) as Element of R;

        set p = <*a9*>;

        take p;

        let i be set;

        assume

         A3: i in ( dom p);

        take aR, a;

        ( dom p) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A4: i = 1 by A3, TARSKI:def 1;



        thus (p /. i) = (p . i) by A3, PARTFUN1:def 6

        .= (a * aR) by A4, FINSEQ_1: 40;

      end;

    end

    registration

      let R be non empty multLoopStr, A be non empty Subset of R;

      cluster non empty for LinearCombination of A;

      existence

      proof

        set a = the Element of A;

        set u = the Element of R;

        set v = u;

        reconsider p = <*((u * a) * v)*> as FinSequence of the carrier of R;

        take p;

        now

          let i be set;

          assume

           A1: i in ( dom p);

          take u, v, a;

          i in {1} by A1, FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1;

          hence (p /. i) = ((u * a) * v) by FINSEQ_4: 16;

        end;

        hence thesis by Def8;

      end;

      cluster non empty for LeftLinearCombination of A;

      existence

      proof

        set a = the Element of A;

        set u = the Element of R;

        reconsider p = <*(u * a)*> as FinSequence of the carrier of R;

        take p;

        now

          let i be set;

          assume

           A2: i in ( dom p);

          take u, a;

          i in {1} by A2, FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1;

          hence (p /. i) = (u * a) by FINSEQ_4: 16;

        end;

        hence thesis by Def9;

      end;

      cluster non empty for RightLinearCombination of A;

      existence

      proof

        set a = the Element of A;

        set v = the Element of R;

        reconsider p = <*(a * v)*> as FinSequence of the carrier of R;

        take p;

        now

          let i be set;

          assume

           A3: i in ( dom p);

          take v, a;

          i in {1} by A3, FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1;

          hence (p /. i) = (a * v) by FINSEQ_4: 16;

        end;

        hence thesis by Def10;

      end;

    end

    definition

      let R be non empty multLoopStr, A,B be non empty Subset of R, F be LinearCombination of A, G be LinearCombination of B;

      :: original: ^

      redefine

      func F ^ G -> LinearCombination of (A \/ B) ;

      coherence

      proof

        set H = (F ^ G);

        thus H is LinearCombination of (A \/ B)

        proof

          let i be set;

          assume

           A1: i in ( dom H);

          then

          reconsider i as Element of NAT ;

          per cases ;

            suppose

             A2: i in ( dom F);

            then

             A3: (F /. i) = (F . i) & (F . i) = (H . i) by FINSEQ_1:def 7, PARTFUN1:def 6;

            consider u,v be Element of R, a be Element of A such that

             A4: (F /. i) = ((u * a) * v) by A2, Def8;

            a in (A \/ B) by XBOOLE_0:def 3;

            hence thesis by A1, A4, A3, PARTFUN1:def 6;

          end;

            suppose not i in ( dom F);

            then

            consider n be Nat such that

             A5: n in ( dom G) and

             A6: i = (( len F) + n) by A1, FINSEQ_1: 25;



             A7: (G /. n) = (G . n) & (G . n) = (H . i) by A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;

            consider u,v be Element of R, b be Element of B such that

             A8: (G /. n) = ((u * b) * v) by A5, Def8;

            b in (A \/ B) by XBOOLE_0:def 3;

            hence thesis by A1, A8, A7, PARTFUN1:def 6;

          end;

        end;

      end;

    end

    theorem :: IDEAL_1:23



     Th23: for R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LinearCombination of A holds (a * F) is LinearCombination of A

    proof

      let R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LinearCombination of A;

      let i be set;

      assume i in ( dom (a * F));

      then

       A1: i in ( dom F) by POLYNOM1:def 1;

      then

      consider u,v be Element of R, b be Element of A such that

       A2: (F /. i) = ((u * b) * v) by Def8;

      take x = (a * u), v, b;



      thus ((a * F) /. i) = (a * (F /. i)) by A1, POLYNOM1:def 1

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

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

    end;

    theorem :: IDEAL_1:24



     Th24: for R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LinearCombination of A holds (F * a) is LinearCombination of A

    proof

      let R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LinearCombination of A;

      let i be set;

      assume i in ( dom (F * a));

      then

       A1: i in ( dom F) by POLYNOM1:def 2;

      then

      consider u,v be Element of R, b be Element of A such that

       A2: (F /. i) = ((u * b) * v) by Def8;

      take u, x = (v * a), b;



      thus ((F * a) /. i) = ((F /. i) * a) by A1, POLYNOM1:def 2

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

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

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

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

    end;

    theorem :: IDEAL_1:25



     Th25: for R be right_unital non empty multLoopStr, A be non empty Subset of R, f be LeftLinearCombination of A holds f is LinearCombination of A

    proof

      let R be right_unital non empty multLoopStr, A be non empty Subset of R, f be LeftLinearCombination of A;

      let i be set;

      assume i in ( dom f);

      then

      consider r be Element of R, a be Element of A such that

       A1: (f /. i) = (r * a) by Def9;

      (f /. i) = ((r * a) * ( 1. R)) by A1;

      hence thesis;

    end;

    definition

      let R be non empty multLoopStr, A,B be non empty Subset of R, F be LeftLinearCombination of A, G be LeftLinearCombination of B;

      :: original: ^

      redefine

      func F ^ G -> LeftLinearCombination of (A \/ B) ;

      coherence

      proof

        set H = (F ^ G);

        thus H is LeftLinearCombination of (A \/ B)

        proof

          let i be set;

          assume

           A1: i in ( dom H);

          then

          reconsider i as Element of NAT ;

          per cases ;

            suppose

             A2: i in ( dom F);

            then

             A3: (F /. i) = (F . i) & (F . i) = (H . i) by FINSEQ_1:def 7, PARTFUN1:def 6;

            consider u be Element of R, a be Element of A such that

             A4: (F /. i) = (u * a) by A2, Def9;

            a in (A \/ B) by XBOOLE_0:def 3;

            hence thesis by A1, A4, A3, PARTFUN1:def 6;

          end;

            suppose not i in ( dom F);

            then

            consider n be Nat such that

             A5: n in ( dom G) and

             A6: i = (( len F) + n) by A1, FINSEQ_1: 25;



             A7: (G /. n) = (G . n) & (G . n) = (H . i) by A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;

            consider u be Element of R, b be Element of B such that

             A8: (G /. n) = (u * b) by A5, Def9;

            b in (A \/ B) by XBOOLE_0:def 3;

            hence thesis by A1, A8, A7, PARTFUN1:def 6;

          end;

        end;

      end;

    end

    theorem :: IDEAL_1:26



     Th26: for R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LeftLinearCombination of A holds (a * F) is LeftLinearCombination of A

    proof

      let R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LeftLinearCombination of A;

      let i be set;

      assume i in ( dom (a * F));

      then

       A1: i in ( dom F) by POLYNOM1:def 1;

      then

      consider u be Element of R, b be Element of A such that

       A2: (F /. i) = (u * b) by Def9;

      take x = (a * u), b;



      thus ((a * F) /. i) = (a * (F /. i)) by A1, POLYNOM1:def 1

      .= (x * b) by A2, GROUP_1:def 3;

    end;

    theorem :: IDEAL_1:27

    for R be non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LeftLinearCombination of A holds (F * a) is LinearCombination of A

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be LeftLinearCombination of A;

      let i be set;

      reconsider c = a as Element of R;

      assume i in ( dom (F * a));

      then

       A1: i in ( dom F) by POLYNOM1:def 2;

      then

      consider u be Element of R, b be Element of A such that

       A2: (F /. i) = (u * b) by Def9;

      take u, c, b;

      thus thesis by A1, A2, POLYNOM1:def 2;

    end;

    theorem :: IDEAL_1:28



     Th28: for R be left_unital non empty multLoopStr, A be non empty Subset of R, f be RightLinearCombination of A holds f is LinearCombination of A

    proof

      let R be left_unital non empty multLoopStr, A be non empty Subset of R, f be RightLinearCombination of A;

      let i be set;

      assume i in ( dom f);

      then

      consider r be Element of R, a be Element of A such that

       A1: (f /. i) = (a * r) by Def10;

      (f /. i) = ((( 1. R) * a) * r) by A1;

      hence thesis;

    end;

    definition

      let R be non empty multLoopStr, A,B be non empty Subset of R, F be RightLinearCombination of A, G be RightLinearCombination of B;

      :: original: ^

      redefine

      func F ^ G -> RightLinearCombination of (A \/ B) ;

      coherence

      proof

        set H = (F ^ G);

        thus H is RightLinearCombination of (A \/ B)

        proof

          let i be set;

          assume

           A1: i in ( dom H);

          then

          reconsider i as Element of NAT ;

          per cases ;

            suppose

             A2: i in ( dom F);

            then

             A3: (F /. i) = (F . i) & (F . i) = (H . i) by FINSEQ_1:def 7, PARTFUN1:def 6;

            consider u be Element of R, a be Element of A such that

             A4: (F /. i) = (a * u) by A2, Def10;

            a in (A \/ B) by XBOOLE_0:def 3;

            hence thesis by A1, A4, A3, PARTFUN1:def 6;

          end;

            suppose not i in ( dom F);

            then

            consider n be Nat such that

             A5: n in ( dom G) and

             A6: i = (( len F) + n) by A1, FINSEQ_1: 25;



             A7: (G /. n) = (G . n) & (G . n) = (H . i) by A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;

            consider u be Element of R, b be Element of B such that

             A8: (G /. n) = (b * u) by A5, Def10;

            b in (A \/ B) by XBOOLE_0:def 3;

            hence thesis by A1, A8, A7, PARTFUN1:def 6;

          end;

        end;

      end;

    end

    theorem :: IDEAL_1:29



     Th29: for R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be RightLinearCombination of A holds (F * a) is RightLinearCombination of A

    proof

      let R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be RightLinearCombination of A;

      let i be set;

      assume i in ( dom (F * a));

      then

       A1: i in ( dom F) by POLYNOM1:def 2;

      then

      consider u be Element of R, b be Element of A such that

       A2: (F /. i) = (b * u) by Def10;

      take x = (u * a), b;



      thus ((F * a) /. i) = ((F /. i) * a) by A1, POLYNOM1:def 2

      .= (b * x) by A2, GROUP_1:def 3;

    end;

    theorem :: IDEAL_1:30

    for R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be RightLinearCombination of A holds (a * F) is LinearCombination of A

    proof

      let R be associative non empty multLoopStr, A be non empty Subset of R, a be Element of R, F be RightLinearCombination of A;

      let i be set;

      reconsider c = a as Element of R;

      assume i in ( dom (a * F));

      then

       A1: i in ( dom F) by POLYNOM1:def 1;

      then

      consider u be Element of R, b be Element of A such that

       A2: (F /. i) = (b * u) by Def10;

      take c, u, b;



      thus ((a * F) /. i) = (a * (F /. i)) by A1, POLYNOM1:def 1

      .= ((c * b) * u) by A2, GROUP_1:def 3;

    end;

    theorem :: IDEAL_1:31



     Th31: for R be commutative associative non empty multLoopStr, A be non empty Subset of R, f be LinearCombination of A holds f is LeftLinearCombination of A & f is RightLinearCombination of A

    proof

      let R be commutative associative non empty multLoopStr, A be non empty Subset of R, f be LinearCombination of A;

      hereby

        let i be set;

        assume i in ( dom f);

        then

        consider r,s be Element of R, a be Element of A such that

         A1: (f /. i) = ((r * a) * s) by Def8;

        (f /. i) = ((r * s) * a) by A1, GROUP_1:def 3;

        hence ex r be Element of R, a be Element of A st (f /. i) = (r * a);

      end;

      let i be set;

      assume i in ( dom f);

      then

      consider r,s be Element of R, a be Element of A such that

       A2: (f /. i) = ((r * a) * s) by Def8;

      (f /. i) = (a * (r * s)) by A2, GROUP_1:def 3;

      hence ex r be Element of R, a be Element of A st (f /. i) = (a * r);

    end;

    theorem :: IDEAL_1:32



     Th32: for S be non empty doubleLoopStr, F be non empty Subset of S, lc be non empty LinearCombination of F holds ex p be LinearCombination of F, e be Element of S st lc = (p ^ <*e*>) & <*e*> is LinearCombination of F

    proof

      let S be non empty doubleLoopStr, F be non empty Subset of S, lc be non empty LinearCombination of F;

      ( len lc) <> 0 ;

      then

      consider p be FinSequence of the carrier of S, e be Element of S such that

       A1: lc = (p ^ <*e*>) by FINSEQ_2: 19;

      now

        let i be set;

        assume

         A2: i in ( dom p);

        then

        reconsider i1 = i as Element of NAT ;



         A3: ( dom p) c= ( dom lc) by A1, FINSEQ_1: 26;

        then

        consider u,v be Element of S, a be Element of F such that

         A4: (lc /. i) = ((u * a) * v) by A2, Def8;

        take u, v, a;



        thus (p /. i) = (p . i) by A2, PARTFUN1:def 6

        .= (lc . i1) by A1, A2, FINSEQ_1:def 7

        .= ((u * a) * v) by A2, A3, A4, PARTFUN1:def 6;

      end;

      then

      reconsider p as LinearCombination of F by Def8;



       A5: ( len lc) = (( len p) + 1) by A1, FINSEQ_2: 16;

      take p;

      take e;

      thus lc = (p ^ <*e*>) by A1;

      let i be set such that

       A6: i in ( dom <*e*>);



       A7: ( len lc) in ( dom lc) by FINSEQ_5: 6;

      then

       A8: (lc /. ( len lc)) = (lc . ( len lc)) by PARTFUN1:def 6;

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

      then

       A9: i = 1 by A6, TARSKI:def 1;

      consider u,v be Element of S, a be Element of F such that

       A10: (lc /. ( len lc)) = ((u * a) * v) by A7, Def8;

      take u, v, a;



      thus ( <*e*> /. i) = ( <*e*> . i) by A6, PARTFUN1:def 6

      .= e by A9, FINSEQ_1: 40

      .= ((u * a) * v) by A1, A5, A10, A8, FINSEQ_1: 42;

    end;

    theorem :: IDEAL_1:33



     Th33: for S be non empty doubleLoopStr, F be non empty Subset of S, lc be non empty LeftLinearCombination of F holds ex p be LeftLinearCombination of F, e be Element of S st lc = (p ^ <*e*>) & <*e*> is LeftLinearCombination of F

    proof

      let S be non empty doubleLoopStr, F be non empty Subset of S, lc be non empty LeftLinearCombination of F;

      ( len lc) <> 0 ;

      then

      consider p be FinSequence of the carrier of S, e be Element of S such that

       A1: lc = (p ^ <*e*>) by FINSEQ_2: 19;

      now

        let i be set;

        assume

         A2: i in ( dom p);

        then

        reconsider i1 = i as Element of NAT ;



         A3: ( dom p) c= ( dom lc) by A1, FINSEQ_1: 26;

        then

        consider u be Element of S, a be Element of F such that

         A4: (lc /. i) = (u * a) by A2, Def9;

        take u, a;



        thus (p /. i) = (p . i) by A2, PARTFUN1:def 6

        .= (lc . i1) by A1, A2, FINSEQ_1:def 7

        .= (u * a) by A2, A3, A4, PARTFUN1:def 6;

      end;

      then

      reconsider p as LeftLinearCombination of F by Def9;



       A5: ( len lc) = (( len p) + 1) by A1, FINSEQ_2: 16;

      take p;

      take e;

      thus lc = (p ^ <*e*>) by A1;

      let i be set such that

       A6: i in ( dom <*e*>);



       A7: ( len lc) in ( dom lc) by FINSEQ_5: 6;

      then

       A8: (lc /. ( len lc)) = (lc . ( len lc)) by PARTFUN1:def 6;

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

      then

       A9: i = 1 by A6, TARSKI:def 1;

      consider u be Element of S, a be Element of F such that

       A10: (lc /. ( len lc)) = (u * a) by A7, Def9;

      take u, a;



      thus ( <*e*> /. i) = ( <*e*> . i) by A6, PARTFUN1:def 6

      .= e by A9, FINSEQ_1: 40

      .= (u * a) by A1, A5, A10, A8, FINSEQ_1: 42;

    end;

    theorem :: IDEAL_1:34



     Th34: for S be non empty doubleLoopStr, F be non empty Subset of S, lc be non empty RightLinearCombination of F holds ex p be RightLinearCombination of F, e be Element of S st lc = (p ^ <*e*>) & <*e*> is RightLinearCombination of F

    proof

      let S be non empty doubleLoopStr, F be non empty Subset of S, lc be non empty RightLinearCombination of F;

      ( len lc) <> 0 ;

      then

      consider p be FinSequence of the carrier of S, e be Element of S such that

       A1: lc = (p ^ <*e*>) by FINSEQ_2: 19;

      now

        let i be set;

        assume

         A2: i in ( dom p);

        then

        reconsider i1 = i as Element of NAT ;



         A3: ( dom p) c= ( dom lc) by A1, FINSEQ_1: 26;

        then

        consider u be Element of S, a be Element of F such that

         A4: (lc /. i) = (a * u) by A2, Def10;

        take u, a;



        thus (p /. i) = (p . i) by A2, PARTFUN1:def 6

        .= (lc . i1) by A1, A2, FINSEQ_1:def 7

        .= (a * u) by A2, A3, A4, PARTFUN1:def 6;

      end;

      then

      reconsider p as RightLinearCombination of F by Def10;



       A5: ( len lc) = (( len p) + 1) by A1, FINSEQ_2: 16;

      take p;

      take e;

      thus lc = (p ^ <*e*>) by A1;

      let i be set such that

       A6: i in ( dom <*e*>);



       A7: ( len lc) in ( dom lc) by FINSEQ_5: 6;

      then

       A8: (lc /. ( len lc)) = (lc . ( len lc)) by PARTFUN1:def 6;

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

      then

       A9: i = 1 by A6, TARSKI:def 1;

      consider u be Element of S, a be Element of F such that

       A10: (lc /. ( len lc)) = (a * u) by A7, Def10;

      take u, a;



      thus ( <*e*> /. i) = ( <*e*> . i) by A6, PARTFUN1:def 6

      .= e by A9, FINSEQ_1: 40

      .= (a * u) by A1, A5, A10, A8, FINSEQ_1: 42;

    end;

    definition

      let R be non empty multLoopStr, A be non empty Subset of R, L be LinearCombination of A, E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:];

      :: IDEAL_1:def11

      pred E represents L means ( len E) = ( len L) & for i be set st i in ( dom L) holds (L . i) = ((((E /. i) `1_3 ) * ((E /. i) `2_3 )) * ((E /. i) `3_3 )) & ((E /. i) `2_3 ) in A;

    end

    theorem :: IDEAL_1:35

    for R be non empty multLoopStr, A be non empty Subset of R, L be LinearCombination of A holds ex E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:] st E represents L

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, L be LinearCombination of A;

      set D = [:the carrier of R, the carrier of R, the carrier of R:];

      defpred P[ set, set] means ex x,y,z be Element of R st $2 = [x, y, z] & y in A & (L /. $1) = ((x * y) * z);

       A1:

      now

        let k be Nat;

        assume k in ( Seg ( len L));

        then k in ( dom L) by FINSEQ_1:def 3;

        then

        consider u,v be Element of R, a be Element of A such that

         A2: (L /. k) = ((u * a) * v) by Def8;

        reconsider b = a as Element of R;

        reconsider d = [u, b, v] as Element of D;

        take d;

        thus P[k, d] by A2;

      end;

      consider E be FinSequence of D such that

       A3: ( dom E) = ( Seg ( len L)) and

       A4: for k be Nat st k in ( Seg ( len L)) holds P[k, (E /. k)] from RECDEF_1:sch 17( A1);

      take E;

      thus ( len E) = ( len L) by A3, FINSEQ_1:def 3;

      let i be set such that

       A5: i in ( dom L);

      reconsider k = i as Element of NAT by A5;

      ( dom L) = ( Seg ( len L)) by FINSEQ_1:def 3;

      then

      consider x,y,z be Element of R such that

       A6: (E /. k) = [x, y, z] and

       A7: y in A and

       A8: (L /. k) = ((x * y) * z) by A4, A5;

      thus (L . i) = ((((E /. i) `1_3 ) * ((E /. i) `2_3 )) * ((E /. i) `3_3 )) by A5, A6, A8, PARTFUN1:def 6;

      thus thesis by A6, A7;

    end;

    theorem :: IDEAL_1:36

    for R,S be non empty multLoopStr, F be non empty Subset of R, lc be LinearCombination of F, G be non empty Subset of S, P be Function of the carrier of R, the carrier of S, E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:] st (P .: F) c= G & E represents lc holds ex LC be LinearCombination of G st ( len lc) = ( len LC) & for i be set st i in ( dom LC) holds (LC . i) = (((P . ((E /. i) `1_3 )) * (P . ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 )))

    proof

      let R,S be non empty multLoopStr, F be non empty Subset of R, lc be LinearCombination of F, G be non empty Subset of S, P be Function of the carrier of R, the carrier of S, E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:];

      assume

       A1: (P .: F) c= G;

      deffunc F( Nat) = (((P . ((E /. $1) `1_3 )) * (P . ((E /. $1) `2_3 ))) * (P . ((E /. $1) `3_3 )));

      consider LC be FinSequence of the carrier of S such that

       A2: ( len LC) = ( len lc) and

       A3: for k be Nat st k in ( dom LC) holds (LC . k) = F(k) from FINSEQ_2:sch 1;

      assume

       A4: E represents lc;

      now

        let i be set such that

         A5: i in ( dom LC);

        ( dom lc) = ( dom LC) by A2, FINSEQ_3: 29;

        then ( dom P) = the carrier of R & ((E /. i) `2_3 ) in F by A4, A5, FUNCT_2:def 1;

        then (P . ((E /. i) `2_3 )) in (P .: F) by FUNCT_1:def 6;

        then

        reconsider a = (P . ((E /. i) `2_3 )) as Element of G by A1;

        reconsider u = (P . ((E /. i) `1_3 )), v = (P . ((E /. i) `3_3 )) as Element of S;

        take u, v, a;

        (LC . i) = (LC /. i) by A5, PARTFUN1:def 6;

        hence (LC /. i) = ((u * a) * v) by A3, A5;

      end;

      then

      reconsider LC as LinearCombination of G by Def8;

      take LC;

      thus ( len lc) = ( len LC) by A2;

      let i be set;

      assume i in ( dom LC);

      hence thesis by A3;

    end;

    definition

      let R be non empty multLoopStr, A be non empty Subset of R, L be LeftLinearCombination of A, E be FinSequence of [:the carrier of R, the carrier of R:];

      :: IDEAL_1:def12

      pred E represents L means ( len E) = ( len L) & for i be set st i in ( dom L) holds (L . i) = (((E /. i) `1 ) * ((E /. i) `2 )) & ((E /. i) `2 ) in A;

    end

    theorem :: IDEAL_1:37

    for R be non empty multLoopStr, A be non empty Subset of R, L be LeftLinearCombination of A holds ex E be FinSequence of [:the carrier of R, the carrier of R:] st E represents L

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, L be LeftLinearCombination of A;

      set D = [:the carrier of R, the carrier of R:];

      defpred P[ set, set] means ex x,y be Element of R st $2 = [x, y] & y in A & (L /. $1) = (x * y);

       A1:

      now

        let k be Nat;

        assume k in ( Seg ( len L));

        then k in ( dom L) by FINSEQ_1:def 3;

        then

        consider u be Element of R, a be Element of A such that

         A2: (L /. k) = (u * a) by Def9;

        reconsider b = a as Element of R;

        reconsider d = [u, b] as Element of D;

        take d;

        thus P[k, d] by A2;

      end;

      consider E be FinSequence of D such that

       A3: ( dom E) = ( Seg ( len L)) and

       A4: for k be Nat st k in ( Seg ( len L)) holds P[k, (E /. k)] from RECDEF_1:sch 17( A1);

      take E;

      thus ( len E) = ( len L) by A3, FINSEQ_1:def 3;

      let i be set such that

       A5: i in ( dom L);

      reconsider k = i as Element of NAT by A5;

      ( dom L) = ( Seg ( len L)) by FINSEQ_1:def 3;

      then

      consider x,y be Element of R such that

       A6: (E /. k) = [x, y] and

       A7: y in A and

       A8: (L /. k) = (x * y) by A4, A5;

      thus (L . i) = (((E /. i) `1 ) * ((E /. i) `2 )) by A5, A6, A8, PARTFUN1:def 6;

      thus thesis by A6, A7;

    end;

    theorem :: IDEAL_1:38

    for R,S be non empty multLoopStr, F be non empty Subset of R, lc be LeftLinearCombination of F, G be non empty Subset of S, P be Function of the carrier of R, the carrier of S, E be FinSequence of [:the carrier of R, the carrier of R:] st (P .: F) c= G & E represents lc holds ex LC be LeftLinearCombination of G st ( len lc) = ( len LC) & for i be set st i in ( dom LC) holds (LC . i) = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 )))

    proof

      let R,S be non empty multLoopStr, F be non empty Subset of R, lc be LeftLinearCombination of F, G be non empty Subset of S, P be Function of the carrier of R, the carrier of S, E be FinSequence of [:the carrier of R, the carrier of R:];

      assume

       A1: (P .: F) c= G;

      deffunc F( Nat) = ((P . ((E /. $1) `1 )) * (P . ((E /. $1) `2 )));

      consider LC be FinSequence of the carrier of S such that

       A2: ( len LC) = ( len lc) and

       A3: for k be Nat st k in ( dom LC) holds (LC . k) = F(k) from FINSEQ_2:sch 1;

      assume

       A4: E represents lc;

      now

        let i be set such that

         A5: i in ( dom LC);

        ( dom lc) = ( dom LC) by A2, FINSEQ_3: 29;

        then ( dom P) = the carrier of R & ((E /. i) `2 ) in F by A4, A5, FUNCT_2:def 1;

        then (P . ((E /. i) `2 )) in (P .: F) by FUNCT_1:def 6;

        then

        reconsider a = (P . ((E /. i) `2 )) as Element of G by A1;

        reconsider u = (P . ((E /. i) `1 )) as Element of S;

        take u, a;

        (LC . i) = (LC /. i) by A5, PARTFUN1:def 6;

        hence (LC /. i) = (u * a) by A3, A5;

      end;

      then

      reconsider LC as LeftLinearCombination of G by Def9;

      take LC;

      thus ( len lc) = ( len LC) by A2;

      let i be set;

      assume i in ( dom LC);

      hence thesis by A3;

    end;

    definition

      let R be non empty multLoopStr, A be non empty Subset of R, L be RightLinearCombination of A, E be FinSequence of [:the carrier of R, the carrier of R:];

      :: IDEAL_1:def13

      pred E represents L means ( len E) = ( len L) & for i be set st i in ( dom L) holds (L . i) = (((E /. i) `1 ) * ((E /. i) `2 )) & ((E /. i) `1 ) in A;

    end

    theorem :: IDEAL_1:39

    for R be non empty multLoopStr, A be non empty Subset of R, L be RightLinearCombination of A holds ex E be FinSequence of [:the carrier of R, the carrier of R:] st E represents L

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, L be RightLinearCombination of A;

      set D = [:the carrier of R, the carrier of R:];

      defpred P[ set, set] means ex x,y be Element of R st $2 = [x, y] & x in A & (L /. $1) = (x * y);

       A1:

      now

        let k be Nat;

        assume k in ( Seg ( len L));

        then k in ( dom L) by FINSEQ_1:def 3;

        then

        consider v be Element of R, a be Element of A such that

         A2: (L /. k) = (a * v) by Def10;

        reconsider b = a as Element of R;

        reconsider d = [b, v] as Element of D;

        take d;

        thus P[k, d] by A2;

      end;

      consider E be FinSequence of D such that

       A3: ( dom E) = ( Seg ( len L)) and

       A4: for k be Nat st k in ( Seg ( len L)) holds P[k, (E /. k)] from RECDEF_1:sch 17( A1);

      take E;

      thus ( len E) = ( len L) by A3, FINSEQ_1:def 3;

      let i be set such that

       A5: i in ( dom L);

      reconsider k = i as Element of NAT by A5;

      ( dom L) = ( Seg ( len L)) by FINSEQ_1:def 3;

      then

      consider x,y be Element of R such that

       A6: (E /. k) = [x, y] and

       A7: x in A and

       A8: (L /. k) = (x * y) by A4, A5;

      thus (L . i) = (((E /. i) `1 ) * ((E /. i) `2 )) by A5, A6, A8, PARTFUN1:def 6;

      thus thesis by A6, A7;

    end;

    theorem :: IDEAL_1:40

    for R,S be non empty multLoopStr, F be non empty Subset of R, lc be RightLinearCombination of F, G be non empty Subset of S, P be Function of the carrier of R, the carrier of S, E be FinSequence of [:the carrier of R, the carrier of R:] st (P .: F) c= G & E represents lc holds ex LC be RightLinearCombination of G st ( len lc) = ( len LC) & for i be set st i in ( dom LC) holds (LC . i) = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 )))

    proof

      let R,S be non empty multLoopStr, F be non empty Subset of R, lc be RightLinearCombination of F, G be non empty Subset of S, P be Function of the carrier of R, the carrier of S, E be FinSequence of [:the carrier of R, the carrier of R:];

      assume

       A1: (P .: F) c= G;

      deffunc F( Nat) = ((P . ((E /. $1) `1 )) * (P . ((E /. $1) `2 )));

      consider LC be FinSequence of the carrier of S such that

       A2: ( len LC) = ( len lc) and

       A3: for k be Nat st k in ( dom LC) holds (LC . k) = F(k) from FINSEQ_2:sch 1;

      assume

       A4: E represents lc;

      now

        let i be set such that

         A5: i in ( dom LC);

        ( dom lc) = ( dom LC) by A2, FINSEQ_3: 29;

        then ( dom P) = the carrier of R & ((E /. i) `1 ) in F by A4, A5, FUNCT_2:def 1;

        then (P . ((E /. i) `1 )) in (P .: F) by FUNCT_1:def 6;

        then

        reconsider a = (P . ((E /. i) `1 )) as Element of G by A1;

        reconsider v = (P . ((E /. i) `2 )) as Element of S;

        take v, a;

        (LC . i) = (LC /. i) by A5, PARTFUN1:def 6;

        hence (LC /. i) = (a * v) by A3, A5;

      end;

      then

      reconsider LC as RightLinearCombination of G by Def10;

      take LC;

      thus ( len lc) = ( len LC) by A2;

      let i be set;

      assume i in ( dom LC);

      hence thesis by A3;

    end;

    theorem :: IDEAL_1:41

    for R be non empty multLoopStr, A be non empty Subset of R, l be LinearCombination of A, n be Nat holds (l | ( Seg n)) is LinearCombination of A

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, l be LinearCombination of A, n be Nat;

      reconsider ln = (l | ( Seg n)) as FinSequence of the carrier of R by FINSEQ_1: 18;

      now

        let i be set such that

         A1: i in ( dom ln);



         A2: ( dom ln) c= ( dom l) by RELAT_1: 60;

        then

        consider u,v be Element of R, a be Element of A such that

         A3: (l /. i) = ((u * a) * v) by A1, Def8;

        take u, v, a;



        thus (ln /. i) = (ln . i) by A1, PARTFUN1:def 6

        .= (l . i) by A1, FUNCT_1: 47

        .= ((u * a) * v) by A1, A2, A3, PARTFUN1:def 6;

      end;

      hence thesis by Def8;

    end;

    theorem :: IDEAL_1:42

    for R be non empty multLoopStr, A be non empty Subset of R, l be LeftLinearCombination of A, n be Nat holds (l | ( Seg n)) is LeftLinearCombination of A

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, l be LeftLinearCombination of A, n be Nat;

      reconsider ln = (l | ( Seg n)) as FinSequence of the carrier of R by FINSEQ_1: 18;

      now

        let i be set such that

         A1: i in ( dom ln);



         A2: ( dom ln) c= ( dom l) by RELAT_1: 60;

        then

        consider u be Element of R, a be Element of A such that

         A3: (l /. i) = (u * a) by A1, Def9;

        take u, a;



        thus (ln /. i) = (ln . i) by A1, PARTFUN1:def 6

        .= (l . i) by A1, FUNCT_1: 47

        .= (u * a) by A1, A2, A3, PARTFUN1:def 6;

      end;

      hence thesis by Def9;

    end;

    theorem :: IDEAL_1:43

    for R be non empty multLoopStr, A be non empty Subset of R, l be RightLinearCombination of A, n be Nat holds (l | ( Seg n)) is RightLinearCombination of A

    proof

      let R be non empty multLoopStr, A be non empty Subset of R, l be RightLinearCombination of A, n be Nat;

      reconsider ln = (l | ( Seg n)) as FinSequence of the carrier of R by FINSEQ_1: 18;

      now

        let i be set such that

         A1: i in ( dom ln);



         A2: ( dom ln) c= ( dom l) by RELAT_1: 60;

        then

        consider v be Element of R, a be Element of A such that

         A3: (l /. i) = (a * v) by A1, Def10;

        take v, a;



        thus (ln /. i) = (ln . i) by A1, PARTFUN1:def 6

        .= (l . i) by A1, FUNCT_1: 47

        .= (a * v) by A1, A2, A3, PARTFUN1:def 6;

      end;

      hence thesis by Def10;

    end;

    begin

    definition

      let L be non empty doubleLoopStr, F be Subset of L;

      assume

       A1: F is non empty;

      :: IDEAL_1:def14

      func F -Ideal -> Ideal of L means

      : Def14: F c= it & for I be Ideal of L st F c= I holds it c= I;

      existence

      proof

        set Id = { I where I be Subset of L : F c= I & I is Ideal of L };

        set I = ( meet Id);

        the carrier of L is Ideal of L by Th10;

        then

         A2: the carrier of L in Id;

         A3:

        now

          let X be set;

          assume X in Id;

          then ex X9 be Subset of L st X9 = X & F c= X9 & X9 is Ideal of L;

          hence F c= X;

        end;

        then F c= I by A2, SETFAM_1: 5;

        then

        reconsider I as non empty Subset of L by A1, A2, SETFAM_1: 3;



         A4: I is add-closed

        proof

          let x,y be Element of L;

          assume

           A5: x in I & y in I;

          now

            let X be set;

            assume

             A6: X in Id;

            then

            consider X9 be Subset of L such that

             A7: X9 = X and F c= X9 and

             A8: X9 is Ideal of L;

            x in X & y in X by A5, A6, SETFAM_1:def 1;

            then (x + y) in X9 by A7, A8, Def1;

            hence {(x + y)} c= X by A7, ZFMISC_1: 31;

          end;

          then {(x + y)} c= I by A2, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;



         A9: I is left-ideal

        proof

          let p,x be Element of L;

          assume

           A10: x in I;

          now

            let X be set;

            assume

             A11: X in Id;

            then

            consider X9 be Subset of L such that

             A12: X9 = X and F c= X9 and

             A13: X9 is Ideal of L;

            x in X by A10, A11, SETFAM_1:def 1;

            then (p * x) in X9 by A12, A13, Def2;

            hence {(p * x)} c= X by A12, ZFMISC_1: 31;

          end;

          then {(p * x)} c= I by A2, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;

        I is right-ideal

        proof

          let p,x be Element of L;

          assume

           A14: x in I;

          now

            let X be set;

            assume

             A15: X in Id;

            then

            consider X9 be Subset of L such that

             A16: X9 = X and F c= X9 and

             A17: X9 is Ideal of L;

            x in X by A14, A15, SETFAM_1:def 1;

            then (x * p) in X9 by A16, A17, Def3;

            hence {(x * p)} c= X by A16, ZFMISC_1: 31;

          end;

          then {(x * p)} c= I by A2, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;

        then

        reconsider I as Ideal of L by A4, A9;

        take I;

        now

          let X be Ideal of L;

          assume F c= X;

          then X in Id;

          hence I c= X by SETFAM_1: 3;

        end;

        hence thesis by A2, A3, SETFAM_1: 5;

      end;

      uniqueness ;

      :: IDEAL_1:def15

      func F -LeftIdeal -> LeftIdeal of L means

      : Def15: F c= it & for I be LeftIdeal of L st F c= I holds it c= I;

      existence

      proof

        set Id = { I where I be Subset of L : F c= I & I is LeftIdeal of L };

        set I = ( meet Id);

        the carrier of L is LeftIdeal of L by Th11;

        then

         A18: the carrier of L in Id;

         A19:

        now

          let X be set;

          assume X in Id;

          then ex X9 be Subset of L st X9 = X & F c= X9 & X9 is LeftIdeal of L;

          hence F c= X;

        end;

        then F c= I by A18, SETFAM_1: 5;

        then

        reconsider I as non empty Subset of L by A1, A18, SETFAM_1: 3;



         A20: I is add-closed

        proof

          let x,y be Element of L;

          assume

           A21: x in I & y in I;

          now

            let X be set;

            assume

             A22: X in Id;

            then

            consider X9 be Subset of L such that

             A23: X9 = X and F c= X9 and

             A24: X9 is LeftIdeal of L;

            x in X & y in X by A21, A22, SETFAM_1:def 1;

            then (x + y) in X9 by A23, A24, Def1;

            hence {(x + y)} c= X by A23, ZFMISC_1: 31;

          end;

          then {(x + y)} c= I by A18, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;

        I is left-ideal

        proof

          let p,x be Element of L;

          assume

           A25: x in I;

          now

            let X be set;

            assume

             A26: X in Id;

            then

            consider X9 be Subset of L such that

             A27: X9 = X and F c= X9 and

             A28: X9 is LeftIdeal of L;

            x in X by A25, A26, SETFAM_1:def 1;

            then (p * x) in X9 by A27, A28, Def2;

            hence {(p * x)} c= X by A27, ZFMISC_1: 31;

          end;

          then {(p * x)} c= I by A18, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;

        then

        reconsider I as LeftIdeal of L by A20;

        take I;

        now

          let X be LeftIdeal of L;

          assume F c= X;

          then X in Id;

          hence I c= X by SETFAM_1: 3;

        end;

        hence thesis by A18, A19, SETFAM_1: 5;

      end;

      uniqueness ;

      :: IDEAL_1:def16

      func F -RightIdeal -> RightIdeal of L means

      : Def16: F c= it & for I be RightIdeal of L st F c= I holds it c= I;

      existence

      proof

        set Id = { I where I be Subset of L : F c= I & I is RightIdeal of L };

        set I = ( meet Id);

        the carrier of L is RightIdeal of L by Th12;

        then

         A29: the carrier of L in Id;

         A30:

        now

          let X be set;

          assume X in Id;

          then ex X9 be Subset of L st X9 = X & F c= X9 & X9 is RightIdeal of L;

          hence F c= X;

        end;

        then F c= I by A29, SETFAM_1: 5;

        then

        reconsider I as non empty Subset of L by A1, A29, SETFAM_1: 3;



         A31: I is add-closed

        proof

          let x,y be Element of L;

          assume

           A32: x in I & y in I;

          now

            let X be set;

            assume

             A33: X in Id;

            then

            consider X9 be Subset of L such that

             A34: X9 = X and F c= X9 and

             A35: X9 is RightIdeal of L;

            x in X & y in X by A32, A33, SETFAM_1:def 1;

            then (x + y) in X9 by A34, A35, Def1;

            hence {(x + y)} c= X by A34, ZFMISC_1: 31;

          end;

          then {(x + y)} c= I by A29, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;

        I is right-ideal

        proof

          let p,x be Element of L;

          assume

           A36: x in I;

          now

            let X be set;

            assume

             A37: X in Id;

            then

            consider X9 be Subset of L such that

             A38: X9 = X and F c= X9 and

             A39: X9 is RightIdeal of L;

            x in X by A36, A37, SETFAM_1:def 1;

            then (x * p) in X9 by A38, A39, Def3;

            hence {(x * p)} c= X by A38, ZFMISC_1: 31;

          end;

          then {(x * p)} c= I by A29, SETFAM_1: 5;

          hence thesis by ZFMISC_1: 31;

        end;

        then

        reconsider I as RightIdeal of L by A31;

        take I;

        now

          let X be RightIdeal of L;

          assume F c= X;

          then X in Id;

          hence I c= X by SETFAM_1: 3;

        end;

        hence thesis by A29, A30, SETFAM_1: 5;

      end;

      uniqueness ;

    end

    theorem :: IDEAL_1:44



     Th44: for L be non empty doubleLoopStr, I be Ideal of L holds (I -Ideal ) = I by Def14;

    theorem :: IDEAL_1:45



     Th45: for L be non empty doubleLoopStr, I be LeftIdeal of L holds (I -LeftIdeal ) = I by Def15;

    theorem :: IDEAL_1:46



     Th46: for L be non empty doubleLoopStr, I be RightIdeal of L holds (I -RightIdeal ) = I by Def16;

    definition

      let L be non empty doubleLoopStr, I be Ideal of L;

      :: IDEAL_1:def17

      mode Basis of I -> non empty Subset of L means (it -Ideal ) = I;

      existence

      proof

        take I;

        thus thesis by Th44;

      end;

    end

    theorem :: IDEAL_1:47

    for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds ( {( 0. L)} -Ideal ) = {( 0. L)} by Th44;

    theorem :: IDEAL_1:48

    for L be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr holds ( {( 0. L)} -Ideal ) = {( 0. L)} by Th44;

    theorem :: IDEAL_1:49

    for L be left_zeroed right_zeroed right_add-cancelable right-distributive non empty doubleLoopStr holds ( {( 0. L)} -LeftIdeal ) = {( 0. L)} by Th45;

    theorem :: IDEAL_1:50

    for L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr holds ( {( 0. L)} -RightIdeal ) = {( 0. L)} by Th46;

    theorem :: IDEAL_1:51

    for L be well-unital non empty doubleLoopStr holds ( {( 1. L)} -Ideal ) = the carrier of L

    proof

      let L be well-unital non empty doubleLoopStr;

      the carrier of L c= ( {( 1. L)} -Ideal )

      proof

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x9 = x as Element of L;

        ( 1. L) in {( 1. L)} & {( 1. L)} c= ( {( 1. L)} -Ideal ) by Def14, TARSKI:def 1;

        then (x9 * ( 1. L)) in ( {( 1. L)} -Ideal ) by Def2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: IDEAL_1:52

    for L be right_unital non empty doubleLoopStr holds ( {( 1. L)} -LeftIdeal ) = the carrier of L

    proof

      let L be right_unital non empty doubleLoopStr;

      the carrier of L c= ( {( 1. L)} -LeftIdeal )

      proof

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x9 = x as Element of L;

        ( 1. L) in {( 1. L)} & {( 1. L)} c= ( {( 1. L)} -LeftIdeal ) by Def15, TARSKI:def 1;

        then (x9 * ( 1. L)) in ( {( 1. L)} -LeftIdeal ) by Def2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: IDEAL_1:53

    for L be left_unital non empty doubleLoopStr holds ( {( 1. L)} -RightIdeal ) = the carrier of L

    proof

      let L be left_unital non empty doubleLoopStr;

      the carrier of L c= ( {( 1. L)} -RightIdeal )

      proof

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x9 = x as Element of L;

        ( 1. L) in {( 1. L)} & {( 1. L)} c= ( {( 1. L)} -RightIdeal ) by Def16, TARSKI:def 1;

        then (( 1. L) * x9) in ( {( 1. L)} -RightIdeal ) by Def3;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: IDEAL_1:54

    for L be non empty doubleLoopStr holds (( [#] L) -Ideal ) = the carrier of L by Def14;

    theorem :: IDEAL_1:55

    for L be non empty doubleLoopStr holds (( [#] L) -LeftIdeal ) = the carrier of L by Def15;

    theorem :: IDEAL_1:56

    for L be non empty doubleLoopStr holds (( [#] L) -RightIdeal ) = the carrier of L by Def16;

    theorem :: IDEAL_1:57



     Th57: for L be non empty doubleLoopStr, A,B be non empty Subset of L st A c= B holds (A -Ideal ) c= (B -Ideal )

    proof

      let L be non empty doubleLoopStr, A,B be non empty Subset of L;

      assume

       A1: A c= B;

      B c= (B -Ideal ) by Def14;

      then A c= (B -Ideal ) by A1;

      hence thesis by Def14;

    end;

    theorem :: IDEAL_1:58

    for L be non empty doubleLoopStr, A,B be non empty Subset of L st A c= B holds (A -LeftIdeal ) c= (B -LeftIdeal )

    proof

      let L be non empty doubleLoopStr, A,B be non empty Subset of L;

      assume

       A1: A c= B;

      B c= (B -LeftIdeal ) by Def15;

      then A c= (B -LeftIdeal ) by A1;

      hence thesis by Def15;

    end;

    theorem :: IDEAL_1:59

    for L be non empty doubleLoopStr, A,B be non empty Subset of L st A c= B holds (A -RightIdeal ) c= (B -RightIdeal )

    proof

      let L be non empty doubleLoopStr, A,B be non empty Subset of L;

      assume

       A1: A c= B;

      B c= (B -RightIdeal ) by Def16;

      then A c= (B -RightIdeal ) by A1;

      hence thesis by Def16;

    end;

    theorem :: IDEAL_1:60



     Th60: for L be add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of L, x be set holds x in (F -Ideal ) iff ex f be LinearCombination of F st x = ( Sum f)

    proof

      let L be add-associative right_zeroed add-cancelable left_zeroed associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of L;

      set I = { x where x be Element of L : ex lc be LinearCombination of F st ( Sum lc) = x };



       A1: I c= the carrier of L

      proof

        let x be object;

        assume x in I;

        then ex x9 be Element of L st x9 = x & ex lc be LinearCombination of F st ( Sum lc) = x9;

        hence thesis;

      end;

      let x be set;



       A2: F c= I

      proof

        let x be object;

        assume

         A3: x in F;

        then

        reconsider x as Element of L;

        set lc = <*x*>;

        now

          let i be set;

          assume

           A4: i in ( dom lc);

          ( dom lc) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by A4, TARSKI:def 1;



          then (lc . i) = x by FINSEQ_1: 40

          .= (( 1. L) * x)

          .= ((( 1. L) * x) * ( 1. L));

          hence ex u,v be Element of L, a be Element of F st (lc /. i) = ((u * a) * v) by A3, A4, PARTFUN1:def 6;

        end;

        then

        reconsider lc as LinearCombination of F by Def8;

        ( Sum lc) = x by BINOM: 3;

        hence thesis;

      end;



       A5: I c= (F -Ideal )

      proof

        defpred P[ Nat] means for lc be LinearCombination of F st ( len lc) <= $1 holds ( Sum lc) in (F -Ideal );

        let x be object;

        assume x in I;

        then

        consider x9 be Element of L such that

         A6: x9 = x and

         A7: ex lc be LinearCombination of F st ( Sum lc) = x9;

        consider lc be LinearCombination of F such that

         A8: ( Sum lc) = x9 by A7;



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

        proof

          let k be Nat;

          assume

           A10: P[k];

          thus P[(k + 1)]

          proof

            let lc be LinearCombination of F;

            assume

             A11: ( len lc) <= (k + 1);

            per cases by A11, NAT_1: 8;

              suppose ( len lc) <= k;

              hence thesis by A10;

            end;

              suppose

               A12: ( len lc) = (k + 1);

              then lc is non empty;

              then

              consider q be LinearCombination of F, r be Element of L such that

               A13: lc = (q ^ <*r*>) and

               A14: <*r*> is LinearCombination of F by Th32;

              (k + 1) = (( len q) + ( len <*r*>)) by A12, A13, FINSEQ_1: 22

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

              then

               A15: ( Sum q) in (F -Ideal ) by A10;

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

              then

               A16: 1 in ( dom <*r*>) by TARSKI:def 1;

              then

              consider u,v be Element of L, a be Element of F such that

               A17: ( <*r*> /. 1) = ((u * a) * v) by A14, Def8;

              F c= (F -Ideal ) by Def14;

              then a in (F -Ideal );

              then

               A18: (u * a) in (F -Ideal ) by Def2;



               A19: ( <*r*> /. 1) = ( <*r*> . 1) by A16, PARTFUN1:def 6;

              ( Sum <*r*>) = r by BINOM: 3

              .= ((u * a) * v) by A17, A19, FINSEQ_1: 40;

              then

               A20: ( Sum <*r*>) in (F -Ideal ) by A18, Def3;

              ( Sum lc) = (( Sum q) + ( Sum <*r*>)) by A13, RLVECT_1: 41;

              hence thesis by A15, A20, Def1;

            end;

          end;

        end;



         A21: P[ 0 ]

        proof

          set y = the Element of F;

          let lc be LinearCombination of F;

          assume ( len lc) <= 0 ;

          then lc = ( <*> the carrier of L);

          then

           A22: ( Sum lc) = ( 0. L) by RLVECT_1: 43;

          F c= (F -Ideal ) by Def14;

          then

           A23: y in (F -Ideal );

          (( 0. L) * y) = ( 0. L) by BINOM: 1;

          hence thesis by A22, A23, Def2;

        end;

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

        then P[( len lc)];

        hence thesis by A6, A8;

      end;

      reconsider I as non empty Subset of L by A2, A1;

      reconsider I9 = I as non empty Subset of L;



       A24: I9 is add-closed

      proof

        let x,y be Element of L;

        assume that

         A25: x in I9 and

         A26: y in I9;

        consider x9 be Element of L such that

         A27: x9 = x and

         A28: ex lc be LinearCombination of F st ( Sum lc) = x9 by A25;

        consider lcx be LinearCombination of F such that

         A29: ( Sum lcx) = x9 by A28;

        consider y9 be Element of L such that

         A30: y9 = y and

         A31: ex lc be LinearCombination of F st ( Sum lc) = y9 by A26;

        consider lcy be LinearCombination of F such that

         A32: ( Sum lcy) = y9 by A31;

        ( Sum (lcx ^ lcy)) = (x9 + y9) by A29, A32, RLVECT_1: 41;

        hence thesis by A27, A30;

      end;



       A33: I9 is right-ideal

      proof

        let p,x be Element of L;

        assume x in I9;

        then

        consider x9 be Element of L such that

         A34: x9 = x and

         A35: ex lc be LinearCombination of F st ( Sum lc) = x9;

        consider lcx be LinearCombination of F such that

         A36: ( Sum lcx) = x9 by A35;

        reconsider lcxp = (lcx * p) as LinearCombination of F by Th24;

        (x * p) = ( Sum lcxp) by A34, A36, BINOM: 5;

        hence thesis;

      end;

      I9 is left-ideal

      proof

        let p,x be Element of L;

        assume x in I9;

        then

        consider x9 be Element of L such that

         A37: x9 = x and

         A38: ex lc be LinearCombination of F st ( Sum lc) = x9;

        consider lcx be LinearCombination of F such that

         A39: ( Sum lcx) = x9 by A38;

        reconsider plcx = (p * lcx) as LinearCombination of F by Th23;

        (p * x) = ( Sum plcx) by A37, A39, BINOM: 4;

        hence thesis;

      end;

      then (F -Ideal ) c= I by A2, A24, A33, Def14;

      then

       A40: I = (F -Ideal ) by A5;

      hereby

        assume x in (F -Ideal );

        then ex x9 be Element of L st x9 = x & ex lc be LinearCombination of F st ( Sum lc) = x9 by A40;

        hence ex f be LinearCombination of F st x = ( Sum f);

      end;

      assume ex f be LinearCombination of F st x = ( Sum f);

      hence thesis by A40;

    end;

    theorem :: IDEAL_1:61



     Th61: for L be add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of L, x be set holds x in (F -LeftIdeal ) iff ex f be LeftLinearCombination of F st x = ( Sum f)

    proof

      let L be add-associative right_zeroed add-cancelable left_zeroed associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of L;

      set I = { x where x be Element of L : ex lc be LeftLinearCombination of F st ( Sum lc) = x };



       A1: I c= the carrier of L

      proof

        let x be object;

        assume x in I;

        then ex x9 be Element of L st x9 = x & ex lc be LeftLinearCombination of F st ( Sum lc) = x9;

        hence thesis;

      end;

      let x be set;



       A2: F c= I

      proof

        let x be object;

        assume

         A3: x in F;

        then

        reconsider x as Element of L;

        set lc = <*x*>;

        now

          let i be set;

          assume

           A4: i in ( dom lc);

          ( dom lc) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by A4, TARSKI:def 1;



          then (lc . i) = x by FINSEQ_1: 40

          .= (( 1. L) * x);

          hence ex u be Element of L, a be Element of F st (lc /. i) = (u * a) by A3, A4, PARTFUN1:def 6;

        end;

        then

        reconsider lc as LeftLinearCombination of F by Def9;

        ( Sum lc) = x by BINOM: 3;

        hence thesis;

      end;



       A5: I c= (F -LeftIdeal )

      proof

        defpred P[ Nat] means for lc be LeftLinearCombination of F st ( len lc) <= $1 holds ( Sum lc) in (F -LeftIdeal );

        let x be object;

        assume x in I;

        then

        consider x9 be Element of L such that

         A6: x9 = x and

         A7: ex lc be LeftLinearCombination of F st ( Sum lc) = x9;

        consider lc be LeftLinearCombination of F such that

         A8: ( Sum lc) = x9 by A7;



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

        proof

          let k be Nat;

          assume

           A10: P[k];

          thus P[(k + 1)]

          proof

            let lc be LeftLinearCombination of F;

            assume

             A11: ( len lc) <= (k + 1);

            per cases by A11, NAT_1: 8;

              suppose ( len lc) <= k;

              hence thesis by A10;

            end;

              suppose

               A12: ( len lc) = (k + 1);

              then lc is non empty;

              then

              consider q be LeftLinearCombination of F, r be Element of L such that

               A13: lc = (q ^ <*r*>) and

               A14: <*r*> is LeftLinearCombination of F by Th33;

              (k + 1) = (( len q) + ( len <*r*>)) by A12, A13, FINSEQ_1: 22

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

              then

               A15: ( Sum q) in (F -LeftIdeal ) by A10;

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

              then

               A16: 1 in ( dom <*r*>) by TARSKI:def 1;

              then

              consider u be Element of L, a be Element of F such that

               A17: ( <*r*> /. 1) = (u * a) by A14, Def9;

              F c= (F -LeftIdeal ) by Def15;

              then

               A18: a in (F -LeftIdeal );



               A19: ( <*r*> /. 1) = ( <*r*> . 1) by A16, PARTFUN1:def 6;

              ( Sum <*r*>) = r by BINOM: 3

              .= (u * a) by A17, A19, FINSEQ_1: 40;

              then

               A20: ( Sum <*r*>) in (F -LeftIdeal ) by A18, Def2;

              ( Sum lc) = (( Sum q) + ( Sum <*r*>)) by A13, RLVECT_1: 41;

              hence thesis by A15, A20, Def1;

            end;

          end;

        end;



         A21: P[ 0 ]

        proof

          set y = the Element of F;

          let lc be LeftLinearCombination of F;

          assume ( len lc) <= 0 ;

          then lc = ( <*> the carrier of L);

          then

           A22: ( Sum lc) = ( 0. L) by RLVECT_1: 43;

          F c= (F -LeftIdeal ) by Def15;

          then

           A23: y in (F -LeftIdeal );

          (( 0. L) * y) = ( 0. L) by BINOM: 1;

          hence thesis by A22, A23, Def2;

        end;

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

        then P[( len lc)];

        hence thesis by A6, A8;

      end;

      reconsider I as non empty Subset of L by A2, A1;

      reconsider I9 = I as non empty Subset of L;



       A24: I9 is add-closed

      proof

        let x,y be Element of L;

        assume that

         A25: x in I9 and

         A26: y in I9;

        consider x9 be Element of L such that

         A27: x9 = x and

         A28: ex lc be LeftLinearCombination of F st ( Sum lc) = x9 by A25;

        consider lcx be LeftLinearCombination of F such that

         A29: ( Sum lcx) = x9 by A28;

        consider y9 be Element of L such that

         A30: y9 = y and

         A31: ex lc be LeftLinearCombination of F st ( Sum lc) = y9 by A26;

        consider lcy be LeftLinearCombination of F such that

         A32: ( Sum lcy) = y9 by A31;

        ( Sum (lcx ^ lcy)) = (x9 + y9) by A29, A32, RLVECT_1: 41;

        hence thesis by A27, A30;

      end;

      I9 is left-ideal

      proof

        let p,x be Element of L;

        assume x in I9;

        then

        consider x9 be Element of L such that

         A33: x9 = x and

         A34: ex lc be LeftLinearCombination of F st ( Sum lc) = x9;

        consider lcx be LeftLinearCombination of F such that

         A35: ( Sum lcx) = x9 by A34;

        reconsider plcx = (p * lcx) as LeftLinearCombination of F by Th26;

        (p * x) = ( Sum plcx) by A33, A35, BINOM: 4;

        hence thesis;

      end;

      then (F -LeftIdeal ) c= I by A2, A24, Def15;

      then

       A36: I = (F -LeftIdeal ) by A5;

      hereby

        assume x in (F -LeftIdeal );

        then ex x9 be Element of L st x9 = x & ex lc be LeftLinearCombination of F st ( Sum lc) = x9 by A36;

        hence ex f be LeftLinearCombination of F st x = ( Sum f);

      end;

      assume ex f be LeftLinearCombination of F st x = ( Sum f);

      hence thesis by A36;

    end;

    theorem :: IDEAL_1:62



     Th62: for L be add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of L, x be set holds x in (F -RightIdeal ) iff ex f be RightLinearCombination of F st x = ( Sum f)

    proof

      let L be add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of L;

      set I = { x where x be Element of L : ex lc be RightLinearCombination of F st ( Sum lc) = x };



       A1: I c= the carrier of L

      proof

        let x be object;

        assume x in I;

        then ex x9 be Element of L st x9 = x & ex lc be RightLinearCombination of F st ( Sum lc) = x9;

        hence thesis;

      end;

      let x be set;



       A2: F c= I

      proof

        let x be object;

        assume

         A3: x in F;

        then

        reconsider x as Element of L;

        set lc = <*x*>;

        now

          let i be set;

          assume

           A4: i in ( dom lc);

          ( dom lc) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by A4, TARSKI:def 1;



          then (lc . i) = x by FINSEQ_1: 40

          .= (x * ( 1. L));

          hence ex v be Element of L, a be Element of F st (lc /. i) = (a * v) by A3, A4, PARTFUN1:def 6;

        end;

        then

        reconsider lc as RightLinearCombination of F by Def10;

        ( Sum lc) = x by BINOM: 3;

        hence thesis;

      end;



       A5: I c= (F -RightIdeal )

      proof

        defpred P[ Nat] means for lc be RightLinearCombination of F st ( len lc) <= $1 holds ( Sum lc) in (F -RightIdeal );

        let x be object;

        assume x in I;

        then

        consider x9 be Element of L such that

         A6: x9 = x and

         A7: ex lc be RightLinearCombination of F st ( Sum lc) = x9;

        consider lc be RightLinearCombination of F such that

         A8: ( Sum lc) = x9 by A7;



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

        proof

          let k be Nat;

          assume

           A10: P[k];

          thus P[(k + 1)]

          proof

            let lc be RightLinearCombination of F;

            assume

             A11: ( len lc) <= (k + 1);

            per cases by A11, NAT_1: 8;

              suppose ( len lc) <= k;

              hence thesis by A10;

            end;

              suppose

               A12: ( len lc) = (k + 1);

              then lc is non empty;

              then

              consider q be RightLinearCombination of F, r be Element of L such that

               A13: lc = (q ^ <*r*>) and

               A14: <*r*> is RightLinearCombination of F by Th34;

              (k + 1) = (( len q) + ( len <*r*>)) by A12, A13, FINSEQ_1: 22

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

              then

               A15: ( Sum q) in (F -RightIdeal ) by A10;

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

              then

               A16: 1 in ( dom <*r*>) by TARSKI:def 1;

              then

              consider v be Element of L, a be Element of F such that

               A17: ( <*r*> /. 1) = (a * v) by A14, Def10;

              F c= (F -RightIdeal ) by Def16;

              then

               A18: a in (F -RightIdeal );



               A19: ( <*r*> /. 1) = ( <*r*> . 1) by A16, PARTFUN1:def 6;

              ( Sum <*r*>) = r by BINOM: 3

              .= (a * v) by A17, A19, FINSEQ_1: 40;

              then

               A20: ( Sum <*r*>) in (F -RightIdeal ) by A18, Def3;

              ( Sum lc) = (( Sum q) + ( Sum <*r*>)) by A13, RLVECT_1: 41;

              hence thesis by A15, A20, Def1;

            end;

          end;

        end;



         A21: P[ 0 ]

        proof

          set y = the Element of F;

          let lc be RightLinearCombination of F;

          assume ( len lc) <= 0 ;

          then lc = ( <*> the carrier of L);

          then

           A22: ( Sum lc) = ( 0. L) by RLVECT_1: 43;

          F c= (F -RightIdeal ) by Def16;

          then

           A23: y in (F -RightIdeal );

          (y * ( 0. L)) = ( 0. L) by BINOM: 2;

          hence thesis by A22, A23, Def3;

        end;

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

        then P[( len lc)];

        hence thesis by A6, A8;

      end;

      reconsider I as non empty Subset of L by A2, A1;

      reconsider I9 = I as non empty Subset of L;



       A24: I9 is add-closed

      proof

        let x,y be Element of L;

        assume that

         A25: x in I9 and

         A26: y in I9;

        consider x9 be Element of L such that

         A27: x9 = x and

         A28: ex lc be RightLinearCombination of F st ( Sum lc) = x9 by A25;

        consider lcx be RightLinearCombination of F such that

         A29: ( Sum lcx) = x9 by A28;

        consider y9 be Element of L such that

         A30: y9 = y and

         A31: ex lc be RightLinearCombination of F st ( Sum lc) = y9 by A26;

        consider lcy be RightLinearCombination of F such that

         A32: ( Sum lcy) = y9 by A31;

        ( Sum (lcx ^ lcy)) = (x9 + y9) by A29, A32, RLVECT_1: 41;

        hence thesis by A27, A30;

      end;

      I9 is right-ideal

      proof

        let p,x be Element of L;

        assume x in I9;

        then

        consider x9 be Element of L such that

         A33: x9 = x and

         A34: ex lc be RightLinearCombination of F st ( Sum lc) = x9;

        consider lcx be RightLinearCombination of F such that

         A35: ( Sum lcx) = x9 by A34;

        reconsider lcxp = (lcx * p) as RightLinearCombination of F by Th29;

        (x * p) = ( Sum lcxp) by A33, A35, BINOM: 5;

        hence thesis;

      end;

      then (F -RightIdeal ) c= I by A2, A24, Def16;

      then

       A36: I = (F -RightIdeal ) by A5;

      hereby

        assume x in (F -RightIdeal );

        then ex x9 be Element of L st x9 = x & ex lc be RightLinearCombination of F st ( Sum lc) = x9 by A36;

        hence ex f be RightLinearCombination of F st x = ( Sum f);

      end;

      assume ex f be RightLinearCombination of F st x = ( Sum f);

      hence thesis by A36;

    end;

    theorem :: IDEAL_1:63



     Th63: for R be add-associative left_zeroed right_zeroed add-cancelable well-unital associative commutative distributive non empty doubleLoopStr, F be non empty Subset of R holds (F -Ideal ) = (F -LeftIdeal ) & (F -Ideal ) = (F -RightIdeal )

    proof

      let R be add-associative left_zeroed right_zeroed add-cancelable well-unital associative commutative distributive non empty doubleLoopStr, F be non empty Subset of R;

      now

        let x be object;

        hereby

          assume x in (F -Ideal );

          then

          consider lc be LinearCombination of F such that

           A1: x = ( Sum lc) by Th60;

          lc is LeftLinearCombination of F by Th31;

          hence x in (F -LeftIdeal ) by A1, Th61;

        end;

        assume x in (F -LeftIdeal );

        then

        consider lc be LeftLinearCombination of F such that

         A2: x = ( Sum lc) by Th61;

        lc is LinearCombination of F by Th25;

        hence x in (F -Ideal ) by A2, Th60;

      end;

      hence (F -Ideal ) = (F -LeftIdeal ) by TARSKI: 2;

      now

        let x be object;

        hereby

          assume x in (F -Ideal );

          then

          consider lc be LinearCombination of F such that

           A3: x = ( Sum lc) by Th60;

          lc is RightLinearCombination of F by Th31;

          hence x in (F -RightIdeal ) by A3, Th62;

        end;

        assume x in (F -RightIdeal );

        then

        consider lc be RightLinearCombination of F such that

         A4: x = ( Sum lc) by Th62;

        lc is LinearCombination of F by Th28;

        hence x in (F -Ideal ) by A4, Th60;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: IDEAL_1:64



     Th64: for R be add-associative left_zeroed right_zeroed add-cancelable well-unital associative commutative distributive non empty doubleLoopStr, a be Element of R holds ( {a} -Ideal ) = the set of all (a * r) where r be Element of R

    proof

      let R be add-associative left_zeroed right_zeroed add-cancelable well-unital commutative associative distributive non empty doubleLoopStr, a be Element of R;

      set A = {a};

      reconsider a9 = a as Element of A by TARSKI:def 1;

      set M = the set of all ( Sum s) where s be LinearCombination of A;

      set N = the set of all (a * r) where r be Element of R;



       A1: for u be object holds u in M implies u in N

      proof

        let u be object;

        assume u in M;

        then

        consider s be LinearCombination of A such that

         A2: u = ( Sum s);

        consider f be sequence of the carrier of R such that

         A3: ( Sum s) = (f . ( len s)) and

         A4: (f . 0 ) = ( 0. R) and

         A5: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Element of NAT ] means ex r be Element of R st (f . $1) = (a * r);

         A6:

        now

          let j be Element of NAT ;

          assume that 0 <= j and

           A7: j < ( len s);

          thus P[j] implies P[(j + 1)]

          proof

            assume ex r be Element of R st (f . j) = (a * r);

            then

            consider r1 be Element of R such that

             A8: (f . j) = (a * r1);

            ( 0 + 1) <= (j + 1) & (j + 1) <= ( len s) by A7, NAT_1: 13;

            then (j + 1) in ( Seg ( len s)) by FINSEQ_1: 1;

            then

             A9: (j + 1) in ( dom s) by FINSEQ_1:def 3;

            then

            consider r2,r3 be Element of R, a9 be Element of A such that

             A10: (s /. (j + 1)) = ((r2 * a9) * r3) by Def8;

            (s . (j + 1)) = (s /. (j + 1)) by A9, PARTFUN1:def 6;

            then (f . (j + 1)) = ((f . j) + (s /. (j + 1))) by A5, A7;



            then (f . (j + 1)) = ((a * r1) + ((r2 * a) * r3)) by A8, A10, TARSKI:def 1

            .= ((a * r1) + (a * (r2 * r3))) by GROUP_1:def 3

            .= (a * (r1 + (r2 * r3))) by VECTSP_1:def 7;

            hence thesis;

          end;

        end;

        (f . 0 ) = (a * ( 0. R)) by A4, BINOM: 2;

        then

         A11: P[ 0 ];

        for k be Element of NAT st 0 <= k & k <= ( len s) holds P[k] from INT_1:sch 7( A11, A6);

        then ex r be Element of R st ( Sum s) = (a * r) by A3;

        hence thesis by A2;

      end;

       A12:

      now

        let x be object;

        hereby

          assume x in ( {a} -Ideal );

          then x in ( {a} -RightIdeal ) by Th63;

          then

          consider f be RightLinearCombination of A such that

           A13: x = ( Sum f) by Th62;

          f is LinearCombination of A by Th28;

          hence x in M by A13;

        end;

        assume x in M;

        then ex s be LinearCombination of A st x = ( Sum s);

        hence x in ( {a} -Ideal ) by Th60;

      end;

      for u be object holds u in N implies u in M

      proof

        let u be object;

        assume u in N;

        then

        consider r be Element of R such that

         A14: u = (a * r);

        set s = <*(a * r)*>;

        for i be set st i in ( dom s) holds ex r,t be Element of R, a be Element of A st (s /. i) = ((r * a) * t)

        proof

          let i be set;



           A15: ( len s) = 1 by FINSEQ_1: 40;

          assume i in ( dom s);

          then i in {1} by A15, FINSEQ_1: 2, FINSEQ_1:def 3;

          then i = 1 by TARSKI:def 1;



          then (s /. i) = (a * r) by FINSEQ_4: 16

          .= ((r * a9) * ( 1. R));

          hence thesis;

        end;

        then

        reconsider s as LinearCombination of A by Def8;

        ( Sum s) = (a * r) by BINOM: 3;

        hence thesis by A14;

      end;

      then M = N by A1, TARSKI: 2;

      hence thesis by A12, TARSKI: 2;

    end;

    theorem :: IDEAL_1:65



     Th65: for R be Abelian left_zeroed right_zeroed add-cancelable well-unital add-associative associative commutative distributive non empty doubleLoopStr, a,b be Element of R holds ( {a, b} -Ideal ) = the set of all ((a * r) + (b * s)) where r,s be Element of R

    proof

      let R be Abelian left_zeroed right_zeroed add-cancelable associative well-unital add-associative commutative distributive non empty doubleLoopStr, a,b be Element of R;

      set A = {a, b};

      reconsider a9 = a, b9 = b as Element of A by TARSKI:def 2;

      set M = the set of all ( Sum s) where s be LinearCombination of A;

      set N = the set of all ((a * r) + (b * s)) where r,s be Element of R;



       A1: for u be object holds u in M implies u in N

      proof

        let u be object;

        assume u in M;

        then

        consider s be LinearCombination of A such that

         A2: u = ( Sum s);

        consider f be sequence of the carrier of R such that

         A3: ( Sum s) = (f . ( len s)) and

         A4: (f . 0 ) = ( 0. R) and

         A5: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Element of NAT ] means ex r,s be Element of R st (f . $1) = ((a * r) + (b * s));

         A6:

        now

          let j be Element of NAT ;

          assume that 0 <= j and

           A7: j < ( len s);

          thus P[j] implies P[(j + 1)]

          proof

            ( 0 + 1) <= (j + 1) & (j + 1) <= ( len s) by A7, NAT_1: 13;

            then (j + 1) in ( Seg ( len s)) by FINSEQ_1: 1;

            then

             A8: (j + 1) in ( dom s) by FINSEQ_1:def 3;

            then

             A9: (s /. (j + 1)) = (s . (j + 1)) by PARTFUN1:def 6;

            assume ex r,s be Element of R st (f . j) = ((a * r) + (b * s));

            then

            consider r1,s1 be Element of R such that

             A10: (f . j) = ((a * r1) + (b * s1));

            consider r2,r3 be Element of R, a9 be Element of A such that

             A11: (s /. (j + 1)) = ((r2 * a9) * r3) by A8, Def8;

            per cases by TARSKI:def 2;

              suppose a9 = a;



              then (f . (j + 1)) = (((a * r1) + (b * s1)) + ((r2 * a) * r3)) by A5, A7, A10, A11, A9

              .= (((a * r1) + ((a * r2) * r3)) + (b * s1)) by RLVECT_1:def 3

              .= (((a * r1) + (a * (r2 * r3))) + (b * s1)) by GROUP_1:def 3

              .= ((a * (r1 + (r2 * r3))) + (b * s1)) by VECTSP_1:def 7;

              hence thesis;

            end;

              suppose a9 = b;



              then (f . (j + 1)) = (((a * r1) + (b * s1)) + ((r2 * b) * r3)) by A5, A7, A10, A11, A9

              .= ((a * r1) + ((b * s1) + ((b * r2) * r3))) by RLVECT_1:def 3

              .= ((a * r1) + ((b * s1) + (b * (r2 * r3)))) by GROUP_1:def 3

              .= ((a * r1) + (b * (s1 + (r2 * r3)))) by VECTSP_1:def 7;

              hence thesis;

            end;

          end;

        end;

        (f . 0 ) = (a * ( 0. R)) by A4, BINOM: 2

        .= ((a * ( 0. R)) + ( 0. R)) by RLVECT_1:def 4

        .= ((a * ( 0. R)) + (b * ( 0. R))) by BINOM: 2;

        then

         A12: P[ 0 ];

        for k be Element of NAT st 0 <= k & k <= ( len s) holds P[k] from INT_1:sch 7( A12, A6);

        then ex r,t be Element of R st ( Sum s) = ((a * r) + (b * t)) by A3;

        hence thesis by A2;

      end;

       A13:

      now

        let x be object;

        hereby

          assume x in ( {a, b} -Ideal );

          then x in ( {a, b} -RightIdeal ) by Th63;

          then

          consider f be RightLinearCombination of A such that

           A14: x = ( Sum f) by Th62;

          f is LinearCombination of A by Th28;

          hence x in M by A14;

        end;

        assume x in M;

        then ex s be LinearCombination of A st x = ( Sum s);

        hence x in ( {a, b} -Ideal ) by Th60;

      end;

      for u be object holds u in N implies u in M

      proof

        let u be object;

        assume u in N;

        then

        consider r,t be Element of R such that

         A15: u = ((a * r) + (b * t));

        set s = <*(a * r), (b * t)*>;

        for i be set st i in ( dom s) holds ex r,t be Element of R, a be Element of A st (s /. i) = ((r * a) * t)

        proof

          let i be set;

          assume

           A16: i in ( dom s);

          then i in ( Seg ( len s)) by FINSEQ_1:def 3;

          then

           A17: i in {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

          per cases by A17, TARSKI:def 2;

            suppose i = 1;



            then (s /. i) = (s . 1) by A16, PARTFUN1:def 6

            .= (a * r) by FINSEQ_1: 44

            .= ((( 1. R) * a9) * r);

            hence thesis;

          end;

            suppose i = 2;



            then (s /. i) = (s . 2) by A16, PARTFUN1:def 6

            .= (b * t) by FINSEQ_1: 44

            .= ((( 1. R) * b9) * t);

            hence thesis;

          end;

        end;

        then

        reconsider s as LinearCombination of A by Def8;

        ( Sum s) = ((a * r) + (b * t)) by Th1;

        hence thesis by A15;

      end;

      then M = N by A1, TARSKI: 2;

      hence thesis by A13, TARSKI: 2;

    end;

    theorem :: IDEAL_1:66



     Th66: for R be non empty doubleLoopStr, a be Element of R holds a in ( {a} -Ideal )

    proof

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

      a in {a} & {a} c= ( {a} -Ideal ) by Def14, TARSKI:def 1;

      hence thesis;

    end;

    theorem :: IDEAL_1:67

    for R be Abelian left_zeroed right_zeroed right_complementable add-associative associative commutative distributive well-unital non empty doubleLoopStr, A be non empty Subset of R, a be Element of R holds a in (A -Ideal ) implies ( {a} -Ideal ) c= (A -Ideal )

    proof

      let R be left_zeroed right_zeroed right_complementable add-associative associative distributive well-unital commutative Abelian non empty doubleLoopStr, A be non empty Subset of R, a be Element of R;

      assume a in (A -Ideal );

      then

      consider s be LinearCombination of A such that

       A1: a = ( Sum s) by Th60;

      let u be object;

      assume u in ( {a} -Ideal );

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

      then

      consider r be Element of R such that

       A2: u = (a * r);

      set t = (s * r);



       A3: ( dom s) = ( dom t) by POLYNOM1:def 2;

      for i be set st i in ( dom t) holds ex u,v be Element of R, a be Element of A st (t /. i) = ((u * a) * v)

      proof

        let i be set;

        assume

         A4: i in ( dom t);

        then

        consider u,v be Element of R, b be Element of A such that

         A5: (s /. i) = ((u * b) * v) by A3, Def8;

        (t /. i) = (((u * b) * v) * r) by A3, A4, A5, POLYNOM1:def 2

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

        hence thesis;

      end;

      then

       A6: t is LinearCombination of A by Def8;

      ( Sum t) = u by A1, A2, BINOM: 5;

      hence u in (A -Ideal ) by A6, Th60;

    end;



     Lm2: for a,b be set holds {a} c= {a, b}

    proof

      let a,b be set;

      let u be object;

      assume u in {a};

      then u = a by TARSKI:def 1;

      hence u in {a, b} by TARSKI:def 2;

    end;

    theorem :: IDEAL_1:68

    for R be non empty doubleLoopStr, a,b be Element of R holds a in ( {a, b} -Ideal ) & b in ( {a, b} -Ideal )

    proof

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

      ( {a} -Ideal ) c= ( {a, b} -Ideal ) & a in ( {a} -Ideal ) by Lm2, Th57, Th66;

      hence a in ( {a, b} -Ideal );

      ( {b} -Ideal ) c= ( {a, b} -Ideal ) & b in ( {b} -Ideal ) by Lm2, Th57, Th66;

      hence thesis;

    end;

    theorem :: IDEAL_1:69

    for R be non empty doubleLoopStr, a,b be Element of R holds ( {a} -Ideal ) c= ( {a, b} -Ideal ) & ( {b} -Ideal ) c= ( {a, b} -Ideal ) by Lm2, Th57;

    begin

    definition

      let R be non empty multMagma, I be Subset of R, a be Element of R;

      :: IDEAL_1:def18

      func a * I -> Subset of R equals { (a * i) where i be Element of R : i in I };

      coherence

      proof

        set M = { (a * i) where i be Element of R : i in I };

        M is Subset of R

        proof

          per cases ;

            suppose

             A1: I is empty;

            M is empty

            proof

              assume M is non empty;

              then

              reconsider M as non empty set;

              set b = the Element of M;

              b in { (a * i) where i be Element of R : i in I };

              then ex i be Element of R st b = (a * i) & i in I;

              hence thesis by A1;

            end;

            then for u be object holds u in M implies u in the carrier of R;

            hence thesis by TARSKI:def 3;

          end;

            suppose I is non empty;

            then

            reconsider I as non empty set;

            set j9 = the Element of I;

            j9 in I;

            then

            reconsider j = j9 as Element of R;

            (a * j) in { (a * i) where i be Element of R : i in I };

            then

            reconsider M as non empty set;

            for x be object holds x in M implies x in the carrier of R

            proof

              let x be object;

              assume x in M;

              then ex i be Element of R st x = (a * i) & i in I;

              hence thesis;

            end;

            hence thesis by TARSKI:def 3;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty multLoopStr, I be non empty Subset of R, a be Element of R;

      cluster (a * I) -> non empty;

      coherence

      proof

        set j = the Element of I;

        (a * j) in { (a * i) where i be Element of R : i in I };

        hence thesis;

      end;

    end

    registration

      let R be distributive non empty doubleLoopStr, I be add-closed Subset of R, a be Element of R;

      cluster (a * I) -> add-closed;

      coherence

      proof

        set M = { (a * i) where i be Element of R : i in I };

        for x,y be Element of R st x in M & y in M holds (x + y) in M

        proof

          let x,y be Element of R;

          assume that

           A1: x in M and

           A2: y in M;

          consider i be Element of R such that

           A3: x = (a * i) & i in I by A1;

          consider j be Element of R such that

           A4: y = (a * j) & j in I by A2;

          reconsider k = (i + j) as Element of R;

          k in I & (x + y) = (a * k) by A3, A4, Def1, VECTSP_1:def 7;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let R be associative non empty doubleLoopStr, I be right-ideal Subset of R, a be Element of R;

      cluster (a * I) -> right-ideal;

      coherence

      proof

        set M = { (a * i) where i be Element of R : i in I };

        for y,x be Element of R st x in M holds (x * y) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider i be Element of R such that

           A1: x = (a * i) & i in I;

          (x * y) = (a * (i * y)) & (i * y) in I by A1, Def3, GROUP_1:def 3;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: IDEAL_1:70



     Th70: for R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be non empty Subset of R holds (( 0. R) * I) = {( 0. R)}

    proof

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be non empty Subset of R;

       A1:

      now

        set j = the Element of I;

        let u be object;

        assume u in {( 0. R)};

        then

         A2: u = ( 0. R) by TARSKI:def 1;

        (( 0. R) * j) = ( 0. R) by BINOM: 1;

        hence u in (( 0. R) * I) by A2;

      end;

      now

        let u be object;

        assume u in (( 0. R) * I);

        then ex i be Element of R st u = (( 0. R) * i) & i in I;

        then u = ( 0. R) by BINOM: 1;

        hence u in {( 0. R)} by TARSKI:def 1;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: IDEAL_1:71

    for R be left_unital non empty doubleLoopStr, I be Subset of R holds (( 1. R) * I) = I

    proof

      let R be left_unital non empty doubleLoopStr, I be Subset of R;

       A1:

      now

        let u be object;

        assume

         A2: u in I;

        then

        reconsider u9 = u as Element of R;

        (( 1. R) * u9) = u9;

        hence u in (( 1. R) * I) by A2;

      end;

      now

        let u be object;

        assume u in (( 1. R) * I);

        then ex i be Element of R st u = (( 1. R) * i) & i in I;

        hence u in I;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    definition

      let R be addMagma, I,J be Subset of R;

      :: IDEAL_1:def19

      func I + J -> Subset of R equals { (a + b) where a,b be Element of R : a in I & b in J };

      coherence

      proof

        set M = { (a + b) where a,b be Element of R : a in I & b in J };

        M is Subset of R

        proof

          per cases ;

            suppose

             A1: I is empty or J is empty;

            now

              per cases by A1;

                case

                 A2: I is empty;

                M is empty

                proof

                  assume M is non empty;

                  then

                  reconsider M as non empty set;

                  set x = the Element of M;

                  x in { (a + b) where a,b be Element of R : a in I & b in J };

                  then ex a,b be Element of R st x = (a + b) & a in I & b in J;

                  hence thesis by A2;

                end;

                then for u be object holds u in M implies u in the carrier of R;

                hence thesis by TARSKI:def 3;

              end;

                case

                 A3: J is empty;

                M is empty

                proof

                  assume M is non empty;

                  then

                  reconsider M as non empty set;

                  set x = the Element of M;

                  x in { (a + b) where a,b be Element of R : a in I & b in J };

                  then ex a,b be Element of R st x = (a + b) & a in I & b in J;

                  hence thesis by A3;

                end;

                then for u be object holds u in M implies u in the carrier of R;

                hence thesis by TARSKI:def 3;

              end;

            end;

            hence thesis;

          end;

            suppose

             A4: I is non empty & J is non empty;

            then

            reconsider J as non empty set;

            reconsider I as non empty set by A4;

            set x9 = the Element of I;

            set y9 = the Element of J;

            x9 in I & y9 in J;

            then

            reconsider x = x9, y = y9 as Element of R;

            (x + y) in { (a + b) where a,b be Element of R : a in I & b in J };

            then

            reconsider M as non empty set;

            for x be object holds x in M implies x in the carrier of R

            proof

              let x be object;

              assume x in M;

              then ex a,b be Element of R st x = (a + b) & a in I & b in J;

              hence thesis;

            end;

            hence thesis by TARSKI:def 3;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty addLoopStr, I,J be non empty Subset of R;

      cluster (I + J) -> non empty;

      coherence

      proof

        { (x + y) where x,y be Element of R : x in I & y in J } is non empty

        proof

          set y = the Element of J;

          set x = the Element of I;

          (x + y) in { (a + b) where a,b be Element of R : a in I & b in J };

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let R be Abelian non empty addLoopStr, I,J be Subset of R;

      :: original: +

      redefine

      func I + J;

      commutativity

      proof

        now

          let I,J be Subset of R;

           A1:

          now

            let u be object;

            assume u in (J + I);

            then ex a,b be Element of R st u = (a + b) & a in J & b in I;

            hence u in (I + J);

          end;

          now

            let u be object;

            assume u in (I + J);

            then ex a,b be Element of R st u = (a + b) & a in I & b in J;

            hence u in (J + I);

          end;

          hence (I + J) = (J + I) by A1, TARSKI: 2;

        end;

        hence thesis;

      end;

    end

    registration

      let R be Abelian add-associative non empty addLoopStr, I,J be add-closed Subset of R;

      cluster (I + J) -> add-closed;

      coherence

      proof

        set M = { (a + b) where a,b be Element of R : a in I & b in J };

        for x,y be Element of R st x in M & y in M holds (x + y) in M

        proof

          let x,y be Element of R;

          assume that

           A1: x in M and

           A2: y in M;

          consider a9,b9 be Element of R such that

           A3: x = (a9 + b9) and

           A4: a9 in I & b9 in J by A1;

          consider c,d be Element of R such that

           A5: y = (c + d) and

           A6: c in I & d in J by A2;



           A7: ((a9 + c) + (b9 + d)) = (((a9 + c) + b9) + d) by RLVECT_1:def 3

          .= ((c + x) + d) by A3, RLVECT_1:def 3

          .= (x + y) by A5, RLVECT_1:def 3;

          (a9 + c) in I & (b9 + d) in J by A4, A6, Def1;

          hence thesis by A7;

        end;

        hence thesis;

      end;

    end

    registration

      let R be left-distributive non empty doubleLoopStr, I,J be right-ideal Subset of R;

      cluster (I + J) -> right-ideal;

      coherence

      proof

        set M = { (a + b) where a,b be Element of R : a in I & b in J };

        for y,x be Element of R st x in M holds (x * y) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider a9,b9 be Element of R such that

           A1: x = (a9 + b9) and

           A2: a9 in I & b9 in J;



           A3: ((a9 * y) + (b9 * y)) = (x * y) by A1, VECTSP_1:def 3;

          (a9 * y) in I & (b9 * y) in J by A2, Def3;

          hence thesis by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let R be right-distributive non empty doubleLoopStr, I,J be left-ideal Subset of R;

      cluster (I + J) -> left-ideal;

      coherence

      proof

        set M = { (a + b) where a,b be Element of R : a in I & b in J };

        for y,x be Element of R st x in M holds (y * x) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider a9,b9 be Element of R such that

           A1: x = (a9 + b9) and

           A2: a9 in I & b9 in J;



           A3: ((y * a9) + (y * b9)) = (y * x) by A1, VECTSP_1:def 2;

          (y * a9) in I & (y * b9) in J by A2, Def2;

          hence thesis by A3;

        end;

        hence thesis;

      end;

    end

    theorem :: IDEAL_1:72

    for R be add-associative non empty addLoopStr, I,J,K be Subset of R holds (I + (J + K)) = ((I + J) + K)

    proof

      let R be add-associative non empty addLoopStr, I,J,K be Subset of R;

       A1:

      now

        let u be object;

        assume u in ((I + J) + K);

        then

        consider a,b be Element of R such that

         A2: u = (a + b) and

         A3: a in (I + J) and

         A4: b in K;

        consider c,d be Element of R such that

         A5: a = (c + d) and

         A6: c in I and

         A7: d in J by A3;

        (d + b) in { (a9 + b9) where a9,b9 be Element of R : a9 in J & b9 in K } by A4, A7;

        then (c + (d + b)) in { (a9 + b9) where a9,b9 be Element of R : a9 in I & b9 in (J + K) } by A6;

        hence u in (I + (J + K)) by A2, A5, RLVECT_1:def 3;

      end;

      now

        let u be object;

        assume u in (I + (J + K));

        then

        consider a,b be Element of R such that

         A8: u = (a + b) and

         A9: a in I and

         A10: b in (J + K);

        consider c,d be Element of R such that

         A11: b = (c + d) and

         A12: c in J and

         A13: d in K by A10;

        (a + c) in { (a9 + b9) where a9,b9 be Element of R : a9 in I & b9 in J } by A9, A12;

        then ((a + c) + d) in { (a9 + b9) where a9,b9 be Element of R : a9 in (I + J) & b9 in K } by A13;

        hence u in ((I + J) + K) by A8, A11, RLVECT_1:def 3;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: IDEAL_1:73



     Th73: for R be left_zeroed right_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I,J be right-ideal non empty Subset of R holds I c= (I + J)

    proof

      let R be left_zeroed right_add-cancelable right_zeroed right-distributive non empty doubleLoopStr, I,J be right-ideal non empty Subset of R;

      let u be object;

      assume u in I;

      then

      reconsider u9 = u as Element of I;

      ( 0. R) is Element of J by Th3;

      then (u9 + ( 0. R)) in { (a + b) where a,b be Element of R : a in I & b in J };

      hence u in (I + J) by RLVECT_1:def 4;

    end;

    theorem :: IDEAL_1:74



     Th74: for R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I,J be right-ideal non empty Subset of R holds J c= (I + J)

    proof

      let R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I,J be right-ideal non empty Subset of R;

      let u be object;

      assume u in J;

      then

      reconsider u9 = u as Element of J;

      ( 0. R) is Element of I by Th3;

      then (( 0. R) + u9) in { (a + b) where a,b be Element of R : a in I & b in J };

      hence u in (I + J) by ALGSTR_1:def 2;

    end;

    theorem :: IDEAL_1:75

    for R be non empty addLoopStr, I,J be Subset of R, K be add-closed Subset of R st I c= K & J c= K holds (I + J) c= K

    proof

      let R be non empty addLoopStr, I,J be Subset of R, K be add-closed Subset of R;

      assume

       A1: I c= K & J c= K;

      let u be object;

      assume u in (I + J);

      then ex i,j be Element of R st u = (i + j) & i in I & j in J;

      hence u in K by A1, Def1;

    end;

    theorem :: IDEAL_1:76

    for R be Abelian left_zeroed right_zeroed add-cancelable well-unital add-associative associative commutative distributive non empty doubleLoopStr, a,b be Element of R holds ( {a, b} -Ideal ) = (( {a} -Ideal ) + ( {b} -Ideal ))

    proof

      let R be Abelian left_zeroed right_zeroed add-cancelable well-unital add-associative associative commutative distributive non empty doubleLoopStr, a,b be Element of R;

       A1:

      now

        let u be object;

        assume u in ( {a, b} -Ideal );

        then u in the set of all ((a * r) + (b * s)) where r,s be Element of R by Th65;

        then

        consider r,s be Element of R such that

         A2: u = ((a * r) + (b * s));

        (b * s) in the set of all (b * v) where v be Element of R;

        then

        reconsider b9 = (b * s) as Element of ( {b} -Ideal ) by Th64;

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

        then

        reconsider a9 = (a * r) as Element of ( {a} -Ideal ) by Th64;

        (a9 + b9) in { (x + y) where x,y be Element of R : x in ( {a} -Ideal ) & y in ( {b} -Ideal ) };

        hence u in (( {a} -Ideal ) + ( {b} -Ideal )) by A2;

      end;

      now

        let u be object;

        assume u in (( {a} -Ideal ) + ( {b} -Ideal ));

        then

        consider x,y be Element of R such that

         A3: u = (x + y) and

         A4: x in ( {a} -Ideal ) and

         A5: y in ( {b} -Ideal );

        y in the set of all (b * v) where v be Element of R by A5, Th64;

        then

         A6: ex s be Element of R st y = (b * s);

        x in the set of all (a * v) where v be Element of R by A4, Th64;

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

        then u in the set of all ((a * v) + (b * d)) where v,d be Element of R by A3, A6;

        hence u in ( {a, b} -Ideal ) by Th65;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    definition

      let R be non empty 1-sorted, I,J be Subset of R;

      :: original: /\

      redefine

      :: IDEAL_1:def20

      func I /\ J -> Subset of R equals { x where x be Element of R : x in I & x in J };

      coherence

      proof

        (I /\ J) is Subset of R;

        hence thesis;

      end;

      compatibility

      proof

        defpred Q[ set] means $1 in J;

        defpred P[ set] means $1 in I;

        set X = { x where x be Element of R : P[x] & Q[x] }, Y = { x where x be Element of R : P[x] }, Z = { x where x be Element of R : Q[x] };



         A1: Y = I by DOMAIN_1: 22;

        X = (Y /\ Z) from DOMAIN_1:sch 10;

        hence thesis by A1, DOMAIN_1: 22;

      end;

    end

    registration

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I,J be left-ideal non empty Subset of R;

      cluster (I /\ J) -> non empty;

      coherence

      proof

        ( 0. R) in I & ( 0. R) in J by Th2;

        then ( 0. R) in { x where x be Element of R : x in I & x in J };

        hence thesis;

      end;

    end

    registration

      let R be non empty addLoopStr, I,J be add-closed Subset of R;

      cluster (I /\ J) -> add-closed;

      coherence

      proof

        set M = { x where x be Element of R : x in I & x in J };

        M = (I /\ J);

        then

        reconsider M as Subset of R;

        for x,y be Element of R st x in M & y in M holds (x + y) in M

        proof

          let x,y be Element of R;

          assume that

           A1: x in M and

           A2: y in M;

          consider c be Element of R such that

           A3: c = y and

           A4: c in I & c in J by A2;

          consider a be Element of R such that

           A5: x = a and

           A6: a in I & a in J by A1;

          (a + c) in I & (a + c) in J by A6, A4, Def1;

          hence thesis by A5, A3;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty multLoopStr, I,J be left-ideal Subset of R;

      cluster (I /\ J) -> left-ideal;

      coherence

      proof

        set M = { x where x be Element of R : x in I & x in J };

        M = (I /\ J);

        then

        reconsider M as Subset of R;

        for y,x be Element of R st x in M holds (y * x) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider a be Element of R such that

           A1: x = a and

           A2: a in I & a in J;

          (y * a) in I & (y * a) in J by A2, Def2;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be non empty multLoopStr, I,J be right-ideal Subset of R;

      cluster (I /\ J) -> right-ideal;

      coherence

      proof

        set M = { x where x be Element of R : x in I & x in J };

        M = (I /\ J);

        then

        reconsider M as Subset of R;

        for y,x be Element of R st x in M holds (x * y) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider a be Element of R such that

           A1: x = a and

           A2: a in I & a in J;

          (a * y) in I & (a * y) in J by A2, Def3;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: IDEAL_1:77

    for R be Abelian left_zeroed right_zeroed right_complementable left_unital add-associative left-distributive non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of R, J be Subset of R, K be non empty Subset of R st J c= I holds (I /\ (J + K)) = (J + (I /\ K))

    proof

      let R be Abelian left_zeroed right_zeroed right_complementable left_unital add-associative left-distributive non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of R, J be Subset of R, K be non empty Subset of R;

      assume

       A1: J c= I;

       A2:

      now

        let u be object;

        assume u in (J + (I /\ K));

        then

        consider j,ik be Element of R such that

         A3: u = (j + ik) and

         A4: j in J and

         A5: ik in (I /\ K);



         A6: ex z be Element of R st z = ik & z in I & z in K by A5;

        then

        reconsider k9 = ik as Element of K;

        u = (j + k9) by A3;

        then

         A7: u in (J + K) by A4;

        reconsider j9 = j as Element of I by A1, A4;

        reconsider i9 = ik as Element of I by A6;

        u = (j9 + i9) by A3;

        then u in I by Def1;

        hence u in (I /\ (J + K)) by A7;

      end;

      now

        let u be object;

        assume u in (I /\ (J + K));

        then

        consider v be Element of R such that

         A8: u = v and

         A9: v in I and

         A10: v in (J + K);

        consider j,k be Element of R such that

         A11: v = (j + k) and

         A12: j in J and

         A13: k in K by A10;

        reconsider j9 = j as Element of I by A1, A12;

        ( - j9) in I by Th13;

        then ((j9 + k) + ( - j9)) in I by A9, A11, Def1;

        then ((j9 + ( - j9)) + k) in I by RLVECT_1:def 3;

        then (( 0. R) + k) in I by RLVECT_1: 5;

        then k in I by ALGSTR_1:def 2;

        then k in (I /\ K) by A13;

        hence u in (J + (I /\ K)) by A8, A11, A12;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    definition

      let R be non empty doubleLoopStr, I,J be Subset of R;

      :: IDEAL_1:def21

      func I *' J -> Subset of R equals { ( Sum s) where s be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J };

      coherence

      proof

        set M = { ( Sum s) where s be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J };

        now

          let u be object;

          assume u in M;

          then ex s be FinSequence of the carrier of R st u = ( Sum s) & for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J;

          hence u in the carrier of R;

        end;

        then

        reconsider M as Subset of R by TARSKI:def 3;

        M is Subset of R;

        hence thesis;

      end;

    end

    registration

      let R be non empty doubleLoopStr, I,J be Subset of R;

      cluster (I *' J) -> non empty;

      coherence

      proof

        set M = { ( Sum s) where s be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J };

        M is non empty

        proof

          set p = ( <*> the carrier of R);

          for i be Element of NAT st 1 <= i & i <= ( len p) holds ex a,b be Element of R st (p . i) = (a * b) & a in I & b in J;

          then ( Sum p) in M;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let R be commutative non empty doubleLoopStr, I,J be Subset of R;

      :: original: *'

      redefine

      func I *' J;

      commutativity

      proof

        now

          let I,J be Subset of R;

           A1:

          now

            let u be object;

            assume u in (J *' I);

            then

            consider s be FinSequence of the carrier of R such that

             A2: u = ( Sum s) and

             A3: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in J & b in I;

            for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J

            proof

              let i be Element of NAT ;

              assume 1 <= i & i <= ( len s);

              then ex a,b be Element of R st (s . i) = (a * b) & a in J & b in I by A3;

              hence thesis;

            end;

            hence u in (I *' J) by A2;

          end;

          now

            let u be object;

            assume u in (I *' J);

            then

            consider s be FinSequence of the carrier of R such that

             A4: u = ( Sum s) and

             A5: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J;

            for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in J & b in I

            proof

              let i be Element of NAT ;

              assume 1 <= i & i <= ( len s);

              then ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J by A5;

              hence thesis;

            end;

            hence u in (J *' I) by A4;

          end;

          hence (I *' J) = (J *' I) by A1, TARSKI: 2;

        end;

        hence thesis;

      end;

    end

    registration

      let R be right_zeroed add-associative non empty doubleLoopStr, I,J be Subset of R;

      cluster (I *' J) -> add-closed;

      coherence

      proof

        set M = { ( Sum s) where s be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J };

        M = (I *' J);

        then

        reconsider M as non empty Subset of R;

        for x,y be Element of R st x in M & y in M holds (x + y) in M

        proof

          let x,y be Element of R;

          assume that

           A1: x in M and

           A2: y in M;

          consider s be FinSequence of the carrier of R such that

           A3: x = ( Sum s) and

           A4: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J by A1;

          consider t be FinSequence of the carrier of R such that

           A5: y = ( Sum t) and

           A6: for i be Element of NAT st 1 <= i & i <= ( len t) holds ex a,b be Element of R st (t . i) = (a * b) & a in I & b in J by A2;

          set q = (s ^ t);

           A7:

          now

            let i be Element of NAT ;

            assume that

             A8: 1 <= i and

             A9: i <= ( len q);

            thus ex a,r be Element of R st (q . i) = (a * r) & a in I & r in J

            proof

              per cases ;

                suppose

                 A10: i <= ( len s);

                then i in ( Seg ( len s)) by A8, FINSEQ_1: 1;

                then i in ( dom s) by FINSEQ_1:def 3;

                then (q . i) = (s . i) by FINSEQ_1:def 7;

                hence thesis by A4, A8, A10;

              end;

                suppose

                 A11: ( len s) < i;

                then

                reconsider j = (i - ( len s)) as Element of NAT by INT_1: 5;

                (( len s) - ( len s)) < j by A11, XREAL_1: 9;

                then

                 A12: 1 <= j by NAT_1: 14;

                i <= (( len s) + ( len t)) by A9, FINSEQ_1: 22;

                then

                 A13: j <= ((( len s) + ( len t)) - ( len s)) by XREAL_1: 9;

                (t . j) = (q . i) by A9, A11, FINSEQ_1: 24;

                hence thesis by A6, A12, A13;

              end;

            end;

          end;

          ( Sum q) = (x + y) by A3, A5, RLVECT_1: 41;

          hence thesis by A7;

        end;

        hence thesis;

      end;

    end

    registration

      let R be right_zeroed left_add-cancelable associative left-distributive non empty doubleLoopStr, I,J be right-ideal Subset of R;

      cluster (I *' J) -> right-ideal;

      coherence

      proof

        set M = { ( Sum s) where s be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J };

        M = (I *' J);

        then

        reconsider M as non empty Subset of R;

        for y,x be Element of R st x in M holds (x * y) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider s be FinSequence of the carrier of R such that

           A1: x = ( Sum s) and

           A2: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J;

          set q = (s * y);



           A3: ( Seg ( len q)) = ( dom q) by FINSEQ_1:def 3

          .= ( dom s) by POLYNOM1:def 2

          .= ( Seg ( len s)) by FINSEQ_1:def 3;

          then

           A4: ( len q) = ( len s) by FINSEQ_1: 6;

           A5:

          now

            let i be Element of NAT ;

            assume

             A6: 1 <= i & i <= ( len q);

            then

            consider c,r9 be Element of R such that

             A7: (s . i) = (c * r9) and

             A8: c in I & r9 in J by A2, A4;

            i in ( Seg ( len s)) by A3, A6, FINSEQ_1: 1;

            then

             A9: i in ( dom s) by FINSEQ_1:def 3;

            then

             A10: (s /. i) = (c * r9) by A7, PARTFUN1:def 6;

            i in ( Seg ( len q)) by A6, FINSEQ_1: 1;

            then i in ( dom q) by FINSEQ_1:def 3;



            then

             A11: (q . i) = (q /. i) by PARTFUN1:def 6

            .= ((c * r9) * y) by A9, A10, POLYNOM1:def 2

            .= (c * (r9 * y)) by GROUP_1:def 3;

            thus ex b,r be Element of R st (q . i) = (b * r) & b in I & r in J

            proof

              take c, (r9 * y);

              thus thesis by A8, A11, Def3;

            end;

          end;

          ( Sum q) = (( Sum s) * y) by BINOM: 5;

          hence thesis by A1, A5;

        end;

        hence thesis;

      end;

    end

    registration

      let R be left_zeroed right_add-cancelable associative right-distributive non empty doubleLoopStr, I,J be left-ideal Subset of R;

      cluster (I *' J) -> left-ideal;

      coherence

      proof

        set M = { ( Sum s) where s be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J };

        M = (I *' J);

        then

        reconsider M as non empty Subset of R;

        for y,x be Element of R st x in M holds (y * x) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider s be FinSequence of the carrier of R such that

           A1: x = ( Sum s) and

           A2: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J;

          set q = (y * s);



           A3: ( Seg ( len q)) = ( dom q) by FINSEQ_1:def 3

          .= ( dom s) by POLYNOM1:def 1

          .= ( Seg ( len s)) by FINSEQ_1:def 3;

          then

           A4: ( len q) = ( len s) by FINSEQ_1: 6;

           A5:

          now

            let i be Element of NAT ;

            assume

             A6: 1 <= i & i <= ( len q);

            then

            consider c,r9 be Element of R such that

             A7: (s . i) = (c * r9) and

             A8: c in I & r9 in J by A2, A4;

            i in ( Seg ( len s)) by A3, A6, FINSEQ_1: 1;

            then

             A9: i in ( dom s) by FINSEQ_1:def 3;

            then

             A10: (s /. i) = (c * r9) by A7, PARTFUN1:def 6;

            i in ( Seg ( len q)) by A6, FINSEQ_1: 1;

            then i in ( dom q) by FINSEQ_1:def 3;



            then

             A11: (q . i) = (q /. i) by PARTFUN1:def 6

            .= (y * (c * r9)) by A9, A10, POLYNOM1:def 1

            .= ((y * c) * r9) by GROUP_1:def 3;

            thus ex b,r be Element of R st (q . i) = (b * r) & b in I & r in J

            proof

              take (y * c), r9;

              thus thesis by A8, A11, Def2;

            end;

          end;

          ( Sum q) = (y * ( Sum s)) by BINOM: 4;

          hence thesis by A1, A5;

        end;

        hence thesis;

      end;

    end

    theorem :: IDEAL_1:78

    for R be left_zeroed right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be non empty Subset of R holds ( {( 0. R)} *' I) = {( 0. R)}

    proof

      let R be left_zeroed right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be non empty Subset of R;

       A1:

      now

        let u be object;

        assume u in ( {( 0. R)} *' I);

        then

        consider s be FinSequence of the carrier of R such that

         A2: ( Sum s) = u and

         A3: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in {( 0. R)} & b in I;

        now

          per cases ;

            case ( len s) = 0 ;

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

            hence ( Sum s) = ( 0. R) by RLVECT_1: 43;

          end;

            case ( len s) <> 0 ;

            then 1 <= ( len s) by NAT_1: 14;

            then 1 in ( Seg ( len s)) by FINSEQ_1: 1;

            then

             A4: 1 in ( dom s) by FINSEQ_1:def 3;



             A5: for i be Element of NAT st i in ( dom s) holds (s /. i) = ( 0. R)

            proof

              let i be Element of NAT ;

              assume

               A6: i in ( dom s);

              then i in ( Seg ( len s)) by FINSEQ_1:def 3;

              then 1 <= i & i <= ( len s) by FINSEQ_1: 1;

              then

              consider a,b be Element of R such that

               A7: (s . i) = (a * b) and

               A8: a in {( 0. R)} and b in I by A3;



               A9: a = ( 0. R) by A8, TARSKI:def 1;

              (s /. i) = (a * b) by A6, A7, PARTFUN1:def 6;

              hence thesis by A9, BINOM: 1;

            end;

            then for i be Element of NAT st i in ( dom s) & i <> 1 holds (s /. i) = ( 0. R);



            hence ( Sum s) = (s /. 1) by A4, POLYNOM2: 3

            .= ( 0. R) by A4, A5;

          end;

        end;

        hence u in {( 0. R)} by A2, TARSKI:def 1;

      end;

      now

        reconsider o = ( 0. R) as Element of {( 0. R)} by TARSKI:def 1;

        set a = the Element of I;

        let u be object;

        assume

         A10: u in {( 0. R)};

        set q = <*(( 0. R) * a)*>;



         A11: ( len q) = 1 & (q . 1) = (( 0. R) * a) by FINSEQ_1: 40;



         A12: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex b,r be Element of R st (q . i) = (b * r) & b in {( 0. R)} & r in I

        proof

          let i be Element of NAT ;

          assume 1 <= i & i <= ( len q);

          then (q . i) = (o * a) by A11, XXREAL_0: 1;

          hence thesis;

        end;

        ( Sum q) = (( 0. R) * a) by BINOM: 3

        .= ( 0. R) by BINOM: 1

        .= u by A10, TARSKI:def 1;

        hence u in ( {( 0. R)} *' I) by A12;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: IDEAL_1:79



     Th79: for R be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J be add-closed left-ideal non empty Subset of R holds (I *' J) c= (I /\ J)

    proof

      let R be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J be add-closed left-ideal non empty Subset of R;

      let u be object;

      assume u in (I *' J);

      then

      consider s be FinSequence of the carrier of R such that

       A1: ( Sum s) = u and

       A2: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J;

      consider f be sequence of the carrier of R such that

       A3: ( Sum s) = (f . ( len s)) and

       A4: (f . 0 ) = ( 0. R) and

       A5: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      defpred P[ Element of NAT ] means (f . $1) in I & (f . $1) in J;

       A6:

      now

        let j be Element of NAT ;

        assume that 0 <= j and

         A7: j < ( len s);

        thus P[j] implies P[(j + 1)]

        proof



           A8: (j + 1) <= ( len s) & ( 0 + 1) <= (j + 1) by A7, NAT_1: 13;

          then (j + 1) in ( Seg ( len s)) by FINSEQ_1: 1;

          then (j + 1) in ( dom s) by FINSEQ_1:def 3;

          then

           A9: (s . (j + 1)) = (s /. (j + 1)) by PARTFUN1:def 6;

          ex a,b be Element of R st (s . (j + 1)) = (a * b) & a in I & b in J by A2, A8;

          then

           A10: (s /. (j + 1)) in I & (s /. (j + 1)) in J by A9, Def2, Def3;

          assume

           A11: (f . j) in I & (f . j) in J;

          (f . (j + 1)) = ((f . j) + (s /. (j + 1))) by A5, A7, A9;

          hence thesis by A11, A10, Def1;

        end;

      end;



       A12: P[ 0 ] by A4, Th2, Th3;

      for j be Element of NAT st 0 <= j & j <= ( len s) holds P[j] from INT_1:sch 7( A12, A6);

      then ( Sum s) in I & ( Sum s) in J by A3;

      hence u in (I /\ J) by A1;

    end;

    theorem :: IDEAL_1:80



     Th80: for R be Abelian left_zeroed right_zeroed add-cancelable add-associative associative distributive non empty doubleLoopStr, I,J,K be right-ideal non empty Subset of R holds (I *' (J + K)) = ((I *' J) + (I *' K))

    proof

      let R be Abelian left_zeroed right_zeroed add-cancelable add-associative associative distributive non empty doubleLoopStr, I,J,K be right-ideal non empty Subset of R;

       A1:

      now

        let u be object;

        assume u in (I *' (J + K));

        then

        consider s be FinSequence of the carrier of R such that

         A2: ( Sum s) = u and

         A3: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in (J + K);

        consider f be sequence of the carrier of R such that

         A4: ( Sum s) = (f . ( len s)) and

         A5: (f . 0 ) = ( 0. R) and

         A6: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Element of NAT ] means ex x,y be Element of R st (f . $1) = (x + y) & x in (I *' J) & y in (I *' K);

         A7:

        now

          let n be Element of NAT ;

          assume that 0 <= n and

           A8: n < ( len s);

          thus P[n] implies P[(n + 1)]

          proof

            assume ex x,y be Element of R st (f . n) = (x + y) & x in (I *' J) & y in (I *' K);

            then

            consider x,y be Element of R such that

             A9: (f . n) = (x + y) and

             A10: x in (I *' J) and

             A11: y in (I *' K);

            consider p be FinSequence of the carrier of R such that

             A12: ( Sum p) = y and

             A13: for i be Element of NAT st 1 <= i & i <= ( len p) holds ex a,b be Element of R st (p . i) = (a * b) & a in I & b in K by A11;

            consider q be FinSequence of the carrier of R such that

             A14: ( Sum q) = x and

             A15: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex a,b be Element of R st (q . i) = (a * b) & a in I & b in J by A10;



             A16: ( 0 + 1) <= (n + 1) & (n + 1) <= ( len s) by A8, NAT_1: 13;

            then

            consider a,b be Element of R such that

             A17: (s . (n + 1)) = (a * b) and

             A18: a in I and

             A19: b in (J + K) by A3;

            consider c,d be Element of R such that

             A20: b = (c + d) and

             A21: c in J and

             A22: d in K by A19;

            set q1 = (q ^ <*(a * c)*>), p1 = (p ^ <*(a * d)*>);

            (n + 1) in ( Seg ( len s)) by A16, FINSEQ_1: 1;

            then

             A23: (n + 1) in ( dom s) by FINSEQ_1:def 3;

            then

             A24: (s . (n + 1)) = (s /. (n + 1)) by PARTFUN1:def 6;



             A25: ( len p1) = (( len p) + ( len <*(a * d)*>)) by FINSEQ_1: 22

            .= (( len p) + 1) by FINSEQ_1: 40;

            for i be Element of NAT st 1 <= i & i <= ( len p1) holds ex a,b be Element of R st (p1 . i) = (a * b) & a in I & b in K

            proof

              let i be Element of NAT ;

              assume that

               A26: 1 <= i and

               A27: i <= ( len p1);

              per cases ;

                suppose i = ( len p1);

                hence thesis by A18, A22, A25, FINSEQ_1: 42;

              end;

                suppose i <> ( len p1);

                then i < ( len p1) by A27, XXREAL_0: 1;

                then

                 A28: i <= ( len p) by A25, NAT_1: 13;

                then

                consider a,b be Element of R such that

                 A29: (p . i) = (a * b) and

                 A30: a in I & b in K by A13, A26;

                i in ( Seg ( len p)) by A26, A28, FINSEQ_1: 1;

                then i in ( dom p) by FINSEQ_1:def 3;

                then (p1 . i) = (a * b) by A29, FINSEQ_1:def 7;

                hence thesis by A30;

              end;

            end;

            then

             A31: ( Sum p1) in (I *' K);



             A32: ( len q1) = (( len q) + ( len <*(a * c)*>)) by FINSEQ_1: 22

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

            for i be Element of NAT st 1 <= i & i <= ( len q1) holds ex a,b be Element of R st (q1 . i) = (a * b) & a in I & b in J

            proof

              let i be Element of NAT ;

              assume that

               A33: 1 <= i and

               A34: i <= ( len q1);

              per cases ;

                suppose i = ( len q1);

                hence thesis by A18, A21, A32, FINSEQ_1: 42;

              end;

                suppose i <> ( len q1);

                then i < ( len q1) by A34, XXREAL_0: 1;

                then

                 A35: i <= ( len q) by A32, NAT_1: 13;

                then

                consider a,b be Element of R such that

                 A36: (q . i) = (a * b) and

                 A37: a in I & b in J by A15, A33;

                i in ( Seg ( len q)) by A33, A35, FINSEQ_1: 1;

                then i in ( dom q) by FINSEQ_1:def 3;

                then (q1 . i) = (a * b) by A36, FINSEQ_1:def 7;

                hence thesis by A37;

              end;

            end;

            then

             A38: ( Sum q1) in { ( Sum t) where t be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len t) holds ex a,b be Element of R st (t . i) = (a * b) & a in I & b in J };



             A39: (s /. (n + 1)) = (a * (c + d)) by A23, A17, A20, PARTFUN1:def 6

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

            (( Sum q1) + ( Sum p1)) = ((( Sum q) + ( Sum <*(a * c)*>)) + ( Sum p1)) by RLVECT_1: 41

            .= ((( Sum q) + (a * c)) + ( Sum p1)) by BINOM: 3

            .= ((( Sum q) + (a * c)) + (( Sum p) + ( Sum <*(a * d)*>))) by RLVECT_1: 41

            .= ((( Sum q) + (a * c)) + (( Sum p) + (a * d))) by BINOM: 3

            .= (((( Sum q) + (a * c)) + ( Sum p)) + (a * d)) by RLVECT_1:def 3

            .= (((a * c) + (( Sum q) + ( Sum p))) + (a * d)) by RLVECT_1:def 3

            .= ((f . n) + ((a * c) + (a * d))) by A9, A14, A12, RLVECT_1:def 3

            .= (f . (n + 1)) by A6, A8, A24, A39;

            hence thesis by A38, A31;

          end;

        end;



         A40: P[ 0 ]

        proof

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

          thus thesis by A5, Th3, RLVECT_1:def 4;

        end;

        for n be Element of NAT st 0 <= n & n <= ( len s) holds P[n] from INT_1:sch 7( A40, A7);

        then ex x,y be Element of R st ( Sum s) = (x + y) & x in (I *' J) & y in (I *' K) by A4;

        hence u in ((I *' J) + (I *' K)) by A2;

      end;

      now

        let u be object;

        assume u in ((I *' J) + (I *' K));

        then

        consider a,b be Element of R such that

         A41: u = (a + b) and

         A42: a in (I *' J) and

         A43: b in (I *' K);

        consider p be FinSequence of the carrier of R such that

         A44: b = ( Sum p) and

         A45: for i be Element of NAT st 1 <= i & i <= ( len p) holds ex a,b be Element of R st (p . i) = (a * b) & a in I & b in K by A43;

        consider q be FinSequence of the carrier of R such that

         A46: a = ( Sum q) and

         A47: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex a,b be Element of R st (q . i) = (a * b) & a in I & b in J by A42;

        set s = (p ^ q);



         A48: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in (J + K)

        proof

          let i be Element of NAT ;

          assume that

           A49: 1 <= i and

           A50: i <= ( len s);

          i in ( Seg ( len s)) by A49, A50, FINSEQ_1: 1;

          then

           A51: i in ( dom s) by FINSEQ_1:def 3;

          now

            per cases ;

              case

               A52: i <= ( len p);

              then

              consider a,b be Element of R such that

               A53: (p . i) = (a * b) and

               A54: a in I and

               A55: b in K by A45, A49;

              i in ( Seg ( len p)) by A49, A52, FINSEQ_1: 1;

              then i in ( dom p) by FINSEQ_1:def 3;



              then

               A56: (s . i) = (a * b) by A53, FINSEQ_1:def 7

              .= (a * (( 0. R) + b)) by ALGSTR_1:def 2;

              ( 0. R) in J by Th3;

              then (( 0. R) + b) in { (a9 + b9) where a9,b9 be Element of R : a9 in J & b9 in K } by A55;

              hence thesis by A54, A56;

            end;

              case i > ( len p);

              then not i in ( Seg ( len p)) by FINSEQ_1: 1;

              then not i in ( dom p) by FINSEQ_1:def 3;

              then

              consider n be Nat such that

               A57: n in ( dom q) and

               A58: i = (( len p) + n) by A51, FINSEQ_1: 25;

              n in ( Seg ( len q)) by A57, FINSEQ_1:def 3;

              then 1 <= n & n <= ( len q) by FINSEQ_1: 1;

              then

              consider a,b be Element of R such that

               A59: (q . n) = (a * b) and

               A60: a in I and

               A61: b in J by A47, A57;

              ( 0. R) in K by Th3;

              then

               A62: (b + ( 0. R)) in { (a9 + b9) where a9,b9 be Element of R : a9 in J & b9 in K } by A61;

              (s . i) = (q . n) by A57, A58, FINSEQ_1:def 7

              .= (a * (b + ( 0. R))) by A59, RLVECT_1:def 4;

              hence thesis by A60, A62;

            end;

          end;

          hence thesis;

        end;

        ( Sum s) = u by A41, A46, A44, RLVECT_1: 41;

        hence u in (I *' (J + K)) by A48;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: IDEAL_1:81



     Th81: for R be Abelian left_zeroed right_zeroed add-cancelable add-associative commutative associative distributive non empty doubleLoopStr, I,J be right-ideal non empty Subset of R holds ((I + J) *' (I /\ J)) c= (I *' J)

    proof

      let R be Abelian left_zeroed right_zeroed add-cancelable add-associative commutative associative distributive non empty doubleLoopStr, I,J be right-ideal non empty Subset of R;

       A1:

      now

        let u be object;

        assume u in ((I *' (I /\ J)) + (J *' (I /\ J)));

        then

        consider a,b be Element of R such that

         A2: u = (a + b) and

         A3: a in (I *' (I /\ J)) and

         A4: b in (J *' (I /\ J));

        consider s be FinSequence of the carrier of R such that

         A5: b = ( Sum s) and

         A6: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in J & b in (I /\ J) by A4;

        for i be Element of NAT st 1 <= i & i <= ( len s) holds ex x,y be Element of R st (s . i) = (x * y) & x in I & y in J

        proof

          let i be Element of NAT ;

          assume 1 <= i & i <= ( len s);

          then

           A7: ex x,y be Element of R st (s . i) = (x * y) & x in J & y in (I /\ J) by A6;

          (I /\ J) c= I by XBOOLE_1: 17;

          hence thesis by A7;

        end;

        then

         A8: ( Sum s) in { ( Sum t) where t be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len t) holds ex a,b be Element of R st (t . i) = (a * b) & a in I & b in J };

        consider q be FinSequence of the carrier of R such that

         A9: a = ( Sum q) and

         A10: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex a,b be Element of R st (q . i) = (a * b) & a in I & b in (I /\ J) by A3;

        for i be Element of NAT st 1 <= i & i <= ( len q) holds ex x,y be Element of R st (q . i) = (x * y) & x in I & y in J

        proof

          let i be Element of NAT ;

          assume 1 <= i & i <= ( len q);

          then

           A11: ex x,y be Element of R st (q . i) = (x * y) & x in I & y in (I /\ J) by A10;

          (I /\ J) c= J by XBOOLE_1: 17;

          hence thesis by A11;

        end;

        then ( Sum q) in { ( Sum t) where t be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len t) holds ex a,b be Element of R st (t . i) = (a * b) & a in I & b in J };

        hence u in (I *' J) by A2, A9, A5, A8, Def1;

      end;

      ((I + J) *' (I /\ J)) = ((I *' (I /\ J)) + (J *' (I /\ J))) by Th80;

      hence thesis by A1;

    end;

    theorem :: IDEAL_1:82

    for R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I,J be add-closed left-ideal non empty Subset of R holds ((I + J) *' (I /\ J)) c= (I /\ J)

    proof

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I,J be add-closed left-ideal non empty Subset of R;

      let u be object;

      assume u in ((I + J) *' (I /\ J));

      then

      consider s be FinSequence of the carrier of R such that

       A1: u = ( Sum s) and

       A2: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in (I + J) & b in (I /\ J);

      consider f be sequence of the carrier of R such that

       A3: ( Sum s) = (f . ( len s)) and

       A4: (f . 0 ) = ( 0. R) and

       A5: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      defpred P[ Element of NAT ] means (f . $1) in (I /\ J);

       A6:

      now

        let n be Element of NAT ;

        assume that 0 <= n and

         A7: n < ( len s);

        thus P[n] implies P[(n + 1)]

        proof



           A8: ( 0 + 1) <= (n + 1) & (n + 1) <= ( len s) by A7, NAT_1: 13;

          then (n + 1) in ( Seg ( len s)) by FINSEQ_1: 1;

          then (n + 1) in ( dom s) by FINSEQ_1:def 3;

          then

           A9: (s . (n + 1)) = (s /. (n + 1)) by PARTFUN1:def 6;

          assume

           A10: (f . n) in (I /\ J);

          ex x,y be Element of R st (s . (n + 1)) = (x * y) & x in (I + J) & y in (I /\ J) by A2, A8;

          then (s /. (n + 1)) in (I /\ J) by A9, Def2;

          then ((f . n) + (s /. (n + 1))) in (I /\ J) by A10, Def1;

          hence thesis by A5, A7, A9;

        end;

      end;



       A11: P[ 0 ] by A4, Th2;

      for n be Element of NAT st 0 <= n & n <= ( len s) holds P[n] from INT_1:sch 7( A11, A6);

      hence u in (I /\ J) by A1, A3;

    end;

    definition

      let R be addMagma, I,J be Subset of R;

      :: IDEAL_1:def22

      pred I,J are_co-prime means (I + J) = the carrier of R;

    end

    theorem :: IDEAL_1:83



     Th83: for R be left_zeroed left_unital non empty doubleLoopStr, I,J be non empty Subset of R st (I,J) are_co-prime holds (I /\ J) c= ((I + J) *' (I /\ J))

    proof

      let R be left_zeroed left_unital non empty doubleLoopStr, I,J be non empty Subset of R;

      assume (I,J) are_co-prime ;

      then

       A1: (I + J) = the carrier of R;

      let u be object;

      assume

       A2: u in (I /\ J);

      then

      reconsider u9 = u as Element of R;

      set q = <*(( 1. R) * u9)*>;



       A3: ( len q) = 1 by FINSEQ_1: 39;



       A4: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex x,y be Element of R st (q . i) = (x * y) & x in (I + J) & y in (I /\ J)

      proof

        let i be Element of NAT ;

        assume

         A5: 1 <= i & i <= ( len q);

        take ( 1. R), u9;

        i = 1 by A3, A5, XXREAL_0: 1;

        hence thesis by A1, A2, FINSEQ_1: 40;

      end;

      ( Sum q) = (( 1. R) * u9) by BINOM: 3

      .= u9;

      hence u in ((I + J) *' (I /\ J)) by A4;

    end;

    theorem :: IDEAL_1:84

    for R be Abelian left_zeroed right_zeroed add-cancelable add-associative left_unital commutative associative distributive non empty doubleLoopStr, I be add-closed left-ideal right-ideal non empty Subset of R, J be add-closed left-ideal non empty Subset of R st (I,J) are_co-prime holds (I *' J) = (I /\ J)

    proof

      let R be left_zeroed right_zeroed add-cancelable add-associative Abelian commutative associative distributive left_unital non empty doubleLoopStr, I be add-closed left-ideal right-ideal non empty Subset of R, J be add-closed left-ideal non empty Subset of R;



       A1: (I *' J) c= (I /\ J) by Th79;

      assume (I,J) are_co-prime ;

      then

       A2: (I /\ J) c= ((I + J) *' (I /\ J)) by Th83;

      ((I + J) *' (I /\ J)) c= (I *' J) by Th81;

      then (I /\ J) c= (I *' J) by A2;

      hence thesis by A1;

    end;

    definition

      let R be non empty multMagma, I,J be Subset of R;

      :: IDEAL_1:def23

      func I % J -> Subset of R equals { a where a be Element of R : (a * J) c= I };

      coherence

      proof

        set M = { a where a be Element of R : (a * J) c= I };

        for x be object holds x in M implies x in the carrier of R

        proof

          let x be object;

          assume x in M;

          then ex a be Element of R st x = a & (a * J) c= I;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I,J be left-ideal non empty Subset of R;

      cluster (I % J) -> non empty;

      coherence

      proof

        set M = { a where a be Element of R : (a * J) c= I };

        ( 0. R) in I by Th2;

        then for u be object holds u in {( 0. R)} implies u in I by TARSKI:def 1;

        then

         A1: {( 0. R)} c= I;

        (( 0. R) * J) = {( 0. R)} by Th70;

        then ( 0. R) in M by A1;

        hence thesis;

      end;

    end

    registration

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I,J be add-closed left-ideal non empty Subset of R;

      cluster (I % J) -> add-closed;

      coherence

      proof

        set M = { a where a be Element of R : (a * J) c= I };

        M = (I % J);

        then

        reconsider M as non empty Subset of R;

        for x,y be Element of R st x in M & y in M holds (x + y) in M

        proof

          let x,y be Element of R;

          assume that

           A1: x in M and

           A2: y in M;

          consider b be Element of R such that

           A3: y = b and

           A4: (b * J) c= I by A2;

          consider a be Element of R such that

           A5: x = a and

           A6: (a * J) c= I by A1;

          now

            let u be object;

            assume u in ((a + b) * J);

            then

            consider c be Element of R such that

             A7: u = ((a + b) * c) and

             A8: c in J;



             A9: (b * c) in { (b * i) where i be Element of R : i in J } by A8;

            u = ((a * c) + (b * c)) & (a * c) in (a * J) by A7, A8, VECTSP_1:def 3;

            hence u in I by A6, A4, A9, Def1;

          end;

          then ((a + b) * J) c= I;

          hence thesis by A5, A3;

        end;

        hence thesis;

      end;

    end

    registration

      let R be right_zeroed left_add-cancelable left-distributive associative commutative non empty doubleLoopStr, I,J be left-ideal non empty Subset of R;

      cluster (I % J) -> left-ideal;

      coherence

      proof

        set M = { a where a be Element of R : (a * J) c= I };

        M = (I % J);

        then

        reconsider M as non empty Subset of R;

        for y,x be Element of R st x in M holds (y * x) in M

        proof

          let y,x be Element of R;

          assume x in M;

          then

          consider a be Element of R such that

           A1: x = a and

           A2: (a * J) c= I;

          now

            let u be object;

            assume u in ((y * a) * J);

            then

            consider c be Element of R such that

             A3: u = ((y * a) * c) and

             A4: c in J;

            (y * c) in J by A4, Def2;

            then

             A5: (a * (y * c)) in { (a * i) where i be Element of R : i in J };

            u = (a * (y * c)) by A3, GROUP_1:def 3;

            hence u in I by A2, A5;

          end;

          then ((y * a) * J) c= I;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      cluster (I % J) -> right-ideal;

      coherence ;

    end

    theorem :: IDEAL_1:85

    for R be non empty multLoopStr, I be right-ideal non empty Subset of R, J be Subset of R holds I c= (I % J)

    proof

      let R be non empty multLoopStr, I be right-ideal non empty Subset of R, J be Subset of R;

      let u be object;

      assume

       A1: u in I;

      then

      reconsider u9 = u as Element of R;

      now

        let v be object;

        assume v in (u9 * J);

        then ex j be Element of R st v = (u9 * j) & j in J;

        hence v in I by A1, Def3;

      end;

      then (u9 * J) c= I;

      hence u in (I % J);

    end;

    theorem :: IDEAL_1:86

    for R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of R, J be Subset of R holds ((I % J) *' J) c= I

    proof

      let R be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of R, J be Subset of R;

      let u be object;

      assume u in ((I % J) *' J);

      then

      consider s be FinSequence of the carrier of R such that

       A1: ( Sum s) = u and

       A2: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in (I % J) & b in J;

      consider f be sequence of the carrier of R such that

       A3: ( Sum s) = (f . ( len s)) and

       A4: (f . 0 ) = ( 0. R) and

       A5: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      defpred P[ Element of NAT ] means (f . $1) in I;

       A6:

      now

        let j be Element of NAT ;

        assume that 0 <= j and

         A7: j < ( len s);

        thus P[j] implies P[(j + 1)]

        proof



           A8: (j + 1) <= ( len s) & ( 0 + 1) <= (j + 1) by A7, NAT_1: 13;

          then

          consider a,b be Element of R such that

           A9: (s . (j + 1)) = (a * b) and

           A10: a in (I % J) and

           A11: b in J by A2;

          (j + 1) in ( Seg ( len s)) by A8, FINSEQ_1: 1;

          then (j + 1) in ( dom s) by FINSEQ_1:def 3;

          then

           A12: (s . (j + 1)) = (s /. (j + 1)) by PARTFUN1:def 6;

          then

           A13: (f . (j + 1)) = ((f . j) + (s /. (j + 1))) by A5, A7;

          assume

           A14: (f . j) in I;

          consider d be Element of R such that

           A15: a = d and

           A16: (d * J) c= I by A10;

          (a * b) in { (d * i) where i be Element of R : i in J } by A11, A15;

          hence thesis by A14, A12, A13, A9, A16, Def1;

        end;

      end;



       A17: P[ 0 ] by A4, Th2;

      for j be Element of NAT st 0 <= j & j <= ( len s) holds P[j] from INT_1:sch 7( A17, A6);

      hence u in I by A1, A3;

    end;

    theorem :: IDEAL_1:87



     Th87: for R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J be Subset of R holds ((I % J) *' J) c= I

    proof

      let R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J be Subset of R;

      let u be object;

      assume u in ((I % J) *' J);

      then

      consider s be FinSequence of the carrier of R such that

       A1: ( Sum s) = u and

       A2: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in (I % J) & b in J;

      consider f be sequence of the carrier of R such that

       A3: ( Sum s) = (f . ( len s)) and

       A4: (f . 0 ) = ( 0. R) and

       A5: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      defpred P[ Element of NAT ] means (f . $1) in I;

       A6:

      now

        let j be Element of NAT ;

        assume that 0 <= j and

         A7: j < ( len s);

        thus P[j] implies P[(j + 1)]

        proof



           A8: (j + 1) <= ( len s) & ( 0 + 1) <= (j + 1) by A7, NAT_1: 13;

          then

          consider a,b be Element of R such that

           A9: (s . (j + 1)) = (a * b) and

           A10: a in (I % J) and

           A11: b in J by A2;

          (j + 1) in ( Seg ( len s)) by A8, FINSEQ_1: 1;

          then (j + 1) in ( dom s) by FINSEQ_1:def 3;

          then

           A12: (s . (j + 1)) = (s /. (j + 1)) by PARTFUN1:def 6;

          then

           A13: (f . (j + 1)) = ((f . j) + (s /. (j + 1))) by A5, A7;

          assume

           A14: (f . j) in I;

          consider d be Element of R such that

           A15: a = d and

           A16: (d * J) c= I by A10;

          (a * b) in { (d * i) where i be Element of R : i in J } by A11, A15;

          hence thesis by A14, A12, A13, A9, A16, Def1;

        end;

      end;



       A17: P[ 0 ] by A4, Th3;

      for j be Element of NAT st 0 <= j & j <= ( len s) holds P[j] from INT_1:sch 7( A17, A6);

      hence u in I by A1, A3;

    end;

    theorem :: IDEAL_1:88

    for R be left_zeroed right_add-cancelable right-distributive commutative associative non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J,K be Subset of R holds ((I % J) % K) = (I % (J *' K))

    proof

      let R be left_zeroed right_add-cancelable right-distributive commutative associative non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J,K be Subset of R;

       A1:

      now

        let u be object;

        assume u in ((I % J) % K);

        then

        consider a be Element of R such that

         A2: u = a and

         A3: (a * K) c= (I % J);

        now

          let v be object;

          assume v in (a * (J *' K));

          then

          consider b be Element of R such that

           A4: v = (a * b) and

           A5: b in (J *' K);

          consider s be FinSequence of the carrier of R such that

           A6: ( Sum s) = b and

           A7: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in J & b in K by A5;

          set q = (a * s);



           A8: ( dom q) = ( dom s) by POLYNOM1:def 1;



           A9: ( Seg ( len q)) = ( dom q) by FINSEQ_1:def 3

          .= ( dom s) by POLYNOM1:def 1

          .= ( Seg ( len s)) by FINSEQ_1:def 3;

          then

           A10: ( len q) = ( len s) by FINSEQ_1: 6;

          for j be Element of NAT st 1 <= j & j <= ( len q) holds ex c,d be Element of R st (q . j) = (c * d) & c in (I % J) & d in J

          proof

            let j be Element of NAT ;

            assume

             A11: 1 <= j & j <= ( len q);

            then

            consider c,d be Element of R such that

             A12: (s . j) = (c * d) and

             A13: c in J and

             A14: d in K by A7, A10;



             A15: (a * d) in { (a * b9) where b9 be Element of R : b9 in K } by A14;

            j in ( Seg ( len s)) by A9, A11, FINSEQ_1: 1;

            then

             A16: j in ( dom s) by FINSEQ_1:def 3;

            then

             A17: (s /. j) = (c * d) by A12, PARTFUN1:def 6;

            (q . j) = (q /. j) by A8, A16, PARTFUN1:def 6

            .= (a * (c * d)) by A16, A17, POLYNOM1:def 1

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

            hence thesis by A3, A13, A15;

          end;

          then

           A18: ( Sum q) in { ( Sum t) where t be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len t) holds ex a,b be Element of R st (t . i) = (a * b) & a in (I % J) & b in J };



           A19: ((I % J) *' J) c= I by Th87;

          ( Sum q) = v by A4, A6, BINOM: 4;

          hence v in I by A18, A19;

        end;

        then (a * (J *' K)) c= I;

        hence u in (I % (J *' K)) by A2;

      end;

      now

        let u be object;

        assume u in (I % (J *' K));

        then

        consider a be Element of R such that

         A20: u = a and

         A21: (a * (J *' K)) c= I;

        now

          let v be object;

          assume v in (a * K);

          then

          consider b be Element of R such that

           A22: v = (a * b) and

           A23: b in K;

          now

            let z be object;

            assume z in ((a * b) * J);

            then

            consider c be Element of R such that

             A24: z = ((a * b) * c) and

             A25: c in J;



             A26: z = (a * (c * b)) by A24, GROUP_1:def 3;

            set q = <*(c * b)*>;



             A27: ( len q) = 1 by FINSEQ_1: 40;



             A28: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex x,y be Element of R st (q . i) = (x * y) & x in J & y in K

            proof

              let i be Element of NAT ;

              assume 1 <= i & i <= ( len q);



              then (q . i) = (q . 1) by A27, XXREAL_0: 1

              .= (c * b) by FINSEQ_1: 40;

              hence thesis by A23, A25;

            end;

            ( Sum q) = (c * b) by BINOM: 3;

            then (c * b) in { ( Sum t) where t be FinSequence of the carrier of R : for i be Element of NAT st 1 <= i & i <= ( len t) holds ex a,b be Element of R st (t . i) = (a * b) & a in J & b in K } by A28;

            then z in { (a * f) where f be Element of R : f in (J *' K) } by A26;

            hence z in I by A21;

          end;

          then ((a * b) * J) c= I;

          hence v in (I % J) by A22;

        end;

        then (a * K) c= (I % J);

        hence u in ((I % J) % K) by A20;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: IDEAL_1:89

    for R be non empty multLoopStr, I,J,K be Subset of R holds ((J /\ K) % I) = ((J % I) /\ (K % I))

    proof

      let R be non empty multLoopStr, I,J,K be Subset of R;

       A1:

      now

        let u be object;

        assume u in ((J /\ K) % I);

        then

        consider a be Element of R such that

         A2: u = a and

         A3: (a * I) c= (J /\ K);

        now

          let v be object;

          assume v in (a * I);

          then v in (J /\ K) by A3;

          then ex x be Element of R st v = x & x in J & x in K;

          hence v in K;

        end;

        then (a * I) c= K;

        then

         A4: u in (K % I) by A2;

        now

          let v be object;

          assume v in (a * I);

          then v in (J /\ K) by A3;

          then ex x be Element of R st v = x & x in J & x in K;

          hence v in J;

        end;

        then (a * I) c= J;

        then u in (J % I) by A2;

        hence u in ((J % I) /\ (K % I)) by A4;

      end;

      now

        let u be object;

        assume u in ((J % I) /\ (K % I));

        then

         A5: ex x be Element of R st x = u & x in (J % I) & x in (K % I);

        then

        consider a be Element of R such that

         A6: u = a and

         A7: (a * I) c= J;

        ex b be Element of R st u = b & (b * I) c= K by A5;

        then for v be object st v in (a * I) holds v in (J /\ K) by A6, A7;

        then (a * I) c= (J /\ K);

        hence u in ((J /\ K) % I) by A6;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: IDEAL_1:90

    for R be left_zeroed right_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I be add-closed Subset of R, J,K be right-ideal non empty Subset of R holds (I % (J + K)) = ((I % J) /\ (I % K))

    proof

      let R be left_zeroed right_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, I be add-closed Subset of R, J,K be right-ideal non empty Subset of R;

       A1:

      now

        let u be object;

        assume u in (I % (J + K));

        then

        consider a be Element of R such that

         A2: u = a and

         A3: (a * (J + K)) c= I;

        now

          let u be object;

          assume u in (a * J);

          then

           A4: ex j be Element of R st u = (a * j) & j in J;

          J c= (J + K) by Th73;

          then u in { (a * j9) where j9 be Element of R : j9 in (J + K) } by A4;

          hence u in I by A3;

        end;

        then (a * J) c= I;

        then

         A5: u in (I % J) by A2;

        now

          let u be object;

          assume u in (a * K);

          then

           A6: ex j be Element of R st u = (a * j) & j in K;

          K c= (J + K) by Th74;

          then u in { (a * j9) where j9 be Element of R : j9 in (J + K) } by A6;

          hence u in I by A3;

        end;

        then (a * K) c= I;

        then u in (I % K) by A2;

        hence u in ((I % J) /\ (I % K)) by A5;

      end;

      now

        let u be object;

        assume u in ((I % J) /\ (I % K));

        then

         A7: ex x be Element of R st u = x & x in (I % J) & x in (I % K);

        then

        consider a be Element of R such that

         A8: u = a and

         A9: (a * J) c= I;

        consider b be Element of R such that

         A10: u = b and

         A11: (b * K) c= I by A7;

        now

          let v be object;

          assume v in (a * (J + K));

          then

          consider j be Element of R such that

           A12: v = (a * j) and

           A13: j in (J + K);

          consider x9,y be Element of R such that

           A14: j = (x9 + y) and

           A15: x9 in J & y in K by A13;



           A16: (a * x9) in (a * J) & (b * y) in { (b * j9) where j9 be Element of R : j9 in K } by A15;

          v = ((a * x9) + (b * y)) by A8, A10, A12, A14, VECTSP_1:def 2;

          hence v in I by A9, A11, A16, Def1;

        end;

        then (a * (J + K)) c= I;

        hence u in (I % (J + K)) by A8;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    definition

      let R be well-unital non empty doubleLoopStr, I be Subset of R;

      :: IDEAL_1:def24

      func sqrt I -> Subset of R equals { a where a be Element of R : ex n be Element of NAT st (a |^ n) in I };

      coherence

      proof

        set M = { a where a be Element of R : ex n be Element of NAT st (a |^ n) in I };

        for x be object holds x in M implies x in the carrier of R

        proof

          let x be object;

          assume x in M;

          then ex a be Element of R st a = x & ex n be Element of NAT st (a |^ n) in I;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let R be well-unital non empty doubleLoopStr, I be non empty Subset of R;

      cluster ( sqrt I) -> non empty;

      coherence

      proof

        set M = { a where a be Element of R : ex n be Element of NAT st (a |^ n) in I };

        M is non empty

        proof

          set a = the Element of I;

          (a |^ 1) = a by BINOM: 8;

          then a in M;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let R be Abelian add-associative left_zeroed right_zeroed commutative associative add-cancelable distributive well-unital non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R;

      cluster ( sqrt I) -> add-closed;

      coherence

      proof

        set M = { a where a be Element of R : ex n be Element of NAT st (a |^ n) in I };

        M = ( sqrt I);

        then

        reconsider M as non empty Subset of R;

        for x,y be Element of R st x in M & y in M holds (x + y) in M

        proof

          let x,y be Element of R;

          assume that

           A1: x in M and

           A2: y in M;

          consider a be Element of R such that

           A3: x = a and

           A4: ex n be Element of NAT st (a |^ n) in I by A1;

          consider n be Element of NAT such that

           A5: (a |^ n) in I by A4;

          consider b be Element of R such that

           A6: y = b and

           A7: ex m be Element of NAT st (b |^ m) in I by A2;

          consider m be Element of NAT such that

           A8: (b |^ m) in I by A7;

          set p = ((a,b) In_Power (n + m));

          consider f be sequence of the carrier of R such that

           A9: ( Sum p) = (f . ( len p)) and

           A10: (f . 0 ) = ( 0. R) and

           A11: for j be Nat, v be Element of R st j < ( len p) & v = (p . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

          defpred P[ Element of NAT ] means (f . $1) in I;



           A12: for i be Element of NAT st 1 <= i & i <= ( len p) holds (p . i) in I

          proof

            let i be Element of NAT ;

            assume that

             A13: 1 <= i and

             A14: i <= ( len p);

            set r = (i - 1);

            set l = ((n + m) - r);

            (1 - 1) <= (i - 1) by A13, XREAL_1: 9;

            then

            reconsider r as Element of NAT by INT_1: 3;

            i <= ((n + m) + 1) by A14, BINOM:def 7;

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

            then (r - r) <= ((n + m) - r) by XREAL_1: 9;

            then

            reconsider l as Element of NAT by INT_1: 3;

            i in ( Seg ( len p)) by A13, A14, FINSEQ_1: 1;

            then

             A15: i in ( dom p) by FINSEQ_1:def 3;



            then

             A16: (p . i) = (p /. i) by PARTFUN1:def 6

            .= ((((n + m) choose r) * (a |^ l)) * (b |^ r)) by A15, BINOM:def 7;

            per cases ;

              suppose n <= l;

              then

              consider k be Nat such that

               A17: l = (n + k) by NAT_1: 10;

              reconsider k as Element of NAT by ORDINAL1:def 12;

              (a |^ l) = ((a |^ n) * (a |^ k)) by A17, BINOM: 10;

              then (a |^ l) in I by A5, Def3;

              then (((n + m) choose r) * (a |^ l)) in I by Th17;

              hence thesis by A16, Def3;

            end;

              suppose l < n;

              then (((n + m) + ( - r)) + r) < (n + r) by XREAL_1: 6;

              then (( - n) + (n + m)) < (( - n) + (n + r)) by XREAL_1: 6;

              then

              consider k be Nat such that

               A18: r = (m + k) by NAT_1: 10;

              reconsider k as Element of NAT by ORDINAL1:def 12;

              (b |^ r) = ((b |^ m) * (b |^ k)) by A18, BINOM: 10;

              then (b |^ r) in I by A8, Def3;

              hence thesis by A16, Def3;

            end;

          end;

           A19:

          now

            let j be Element of NAT ;

            assume that 0 <= j and

             A20: j < ( len p);

            thus P[j] implies P[(j + 1)]

            proof

              assume

               A21: (f . j) in I;



               A22: (j + 1) <= ( len p) by A20, NAT_1: 13;

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

              then (j + 1) in ( Seg ( len p)) by A22, FINSEQ_1: 1;

              then (j + 1) in ( dom p) by FINSEQ_1:def 3;

              then

               A23: (p /. (j + 1)) = (p . (j + 1)) by PARTFUN1:def 6;

              then

               A24: (p /. (j + 1)) in I by A12, A22, NAT_1: 11;

              (f . (j + 1)) = ((f . j) + (p /. (j + 1))) by A11, A20, A23;

              hence thesis by A21, A24, Def1;

            end;

          end;



           A25: ((a + b) |^ (n + m)) = ( Sum ((a,b) In_Power (n + m))) by BINOM: 25;



           A26: P[ 0 ] by A10, Th2;

          for i be Element of NAT st 0 <= i & i <= ( len p) holds P[i] from INT_1:sch 7( A26, A19);

          then ((a + b) |^ (n + m)) in I by A25, A9;

          hence thesis by A3, A6;

        end;

        hence thesis;

      end;

    end

    registration

      let R be well-unital commutative associative non empty doubleLoopStr, I be left-ideal non empty Subset of R;

      cluster ( sqrt I) -> left-ideal;

      coherence

      proof

        set M = { a where a be Element of R : ex n be Element of NAT st (a |^ n) in I };

        M = ( sqrt I);

        then

        reconsider M as non empty Subset of R;

        for y,x be Element of R st x in M holds (y * x) in M

        proof

          let y9,x9 be Element of R;

          reconsider x = x9, y = y9 as Element of R;

          assume x9 in M;

          then

          consider a be Element of R such that

           A1: x = a and

           A2: ex n be Element of NAT st (a |^ n) in I;

          consider n be Element of NAT such that

           A3: (a |^ n) in I by A2;



           A4: ((y * a) |^ n) = ((y |^ n) * (a |^ n)) by BINOM: 9;

          ((y |^ n) * (a |^ n)) in I by A3, Def2;

          hence thesis by A1, A4;

        end;

        hence thesis;

      end;

      cluster ( sqrt I) -> right-ideal;

      coherence ;

    end

    theorem :: IDEAL_1:91

    for R be well-unital associative non empty doubleLoopStr, I be non empty Subset of R, a be Element of R holds a in ( sqrt I) iff ex n be Element of NAT st (a |^ n) in ( sqrt I)

    proof

      let R be well-unital associative non empty doubleLoopStr, I be non empty Subset of R, a be Element of R;

       A1:

      now

        assume ex n be Element of NAT st (a |^ n) in ( sqrt I);

        then

        consider n be Element of NAT such that

         A2: (a |^ n) in ( sqrt I);

        consider d be Element of R such that

         A3: (a |^ n) = d and

         A4: ex m be Element of NAT st (d |^ m) in I by A2;

        consider m be Element of NAT such that

         A5: (d |^ m) in I by A4;

        (a |^ (n * m)) = (d |^ m) by A3, BINOM: 11;

        hence a in ( sqrt I) by A5;

      end;

      now



         A6: (a |^ 1) = a by BINOM: 8;

        assume a in ( sqrt I);

        hence ex n be Element of NAT st (a |^ n) in ( sqrt I) by A6;

      end;

      hence thesis by A1;

    end;

    theorem :: IDEAL_1:92

    for R be left_zeroed right_zeroed add-cancelable distributive well-unital associative non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J be add-closed left-ideal non empty Subset of R holds ( sqrt (I *' J)) = ( sqrt (I /\ J))

    proof

      let R be left_zeroed right_zeroed associative add-cancelable distributive well-unital non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, J be add-closed left-ideal non empty Subset of R;

       A1:

      now

        let u be object;

        assume u in ( sqrt (I *' J));

        then

        consider d be Element of R such that

         A2: u = d and

         A3: ex m be Element of NAT st (d |^ m) in (I *' J);

        consider m be Element of NAT such that

         A4: (d |^ m) in (I *' J) by A3;

        consider s be FinSequence of the carrier of R such that

         A5: (d |^ m) = ( Sum s) and

         A6: for i be Element of NAT st 1 <= i & i <= ( len s) holds ex a,b be Element of R st (s . i) = (a * b) & a in I & b in J by A4;

        consider f be sequence of the carrier of R such that

         A7: ( Sum s) = (f . ( len s)) and

         A8: (f . 0 ) = ( 0. R) and

         A9: for j be Nat, v be Element of R st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Element of NAT ] means (f . $1) in (I /\ J);

         A10:

        now

          let j be Element of NAT ;

          assume that 0 <= j and

           A11: j < ( len s);

          thus P[j] implies P[(j + 1)]

          proof

            assume (f . j) in (I /\ J);

            then

             A12: ex g be Element of R st g = (f . j) & g in I & g in J;



             A13: (j + 1) <= ( len s) & ( 0 + 1) <= (j + 1) by A11, NAT_1: 13;

            then

             A14: ex a,b be Element of R st (s . (j + 1)) = (a * b) & a in I & b in J by A6;

            (j + 1) in ( Seg ( len s)) by A13, FINSEQ_1: 1;

            then (j + 1) in ( dom s) by FINSEQ_1:def 3;

            then

             A15: (s . (j + 1)) = (s /. (j + 1)) by PARTFUN1:def 6;

            then

             A16: (f . (j + 1)) = ((f . j) + (s /. (j + 1))) by A9, A11;

            (s /. (j + 1)) in J by A15, A14, Def2;

            then

             A17: (f . (j + 1)) in J by A12, A16, Def1;

            (s /. (j + 1)) in I by A15, A14, Def3;

            then (f . (j + 1)) in I by A12, A16, Def1;

            hence thesis by A17;

          end;

        end;

        (f . 0 ) in I & (f . 0 ) in J by A8, Th2, Th3;

        then

         A18: P[ 0 ];

        for j be Element of NAT st 0 <= j & j <= ( len s) holds P[j] from INT_1:sch 7( A18, A10);

        then ( Sum s) in (I /\ J) by A7;

        hence u in ( sqrt (I /\ J)) by A2, A5;

      end;

      now

        let u be object;

        assume u in ( sqrt (I /\ J));

        then

        consider d be Element of R such that

         A19: u = d and

         A20: ex m be Element of NAT st (d |^ m) in (I /\ J);

        consider m be Element of NAT such that

         A21: (d |^ m) in (I /\ J) by A20;

        set q = <*((d |^ m) * (d |^ m))*>;



         A22: ( len q) = 1 by FINSEQ_1: 40;



         A23: ex g be Element of R st (d |^ m) = g & g in I & g in J by A21;



         A24: for i be Element of NAT st 1 <= i & i <= ( len q) holds ex x,y be Element of R st (q . i) = (x * y) & x in I & y in J

        proof

          let i be Element of NAT ;

          assume

           A25: 1 <= i & i <= ( len q);

          then i in ( Seg ( len q)) by FINSEQ_1: 1;

          then i in ( dom q) by FINSEQ_1:def 3;

          then

           A26: (q . i) = (q /. i) by PARTFUN1:def 6;



          then (q /. i) = (q . 1) by A22, A25, XXREAL_0: 1

          .= ((d |^ m) * (d |^ m)) by FINSEQ_1: 40;

          hence thesis by A23, A26;

        end;

        (d |^ (m + m)) = ((d |^ m) * (d |^ m)) by BINOM: 10

        .= ( Sum q) by BINOM: 3;

        then (d |^ (m + m)) in (I *' J) by A24;

        hence u in ( sqrt (I *' J)) by A19;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    begin

    definition

      let L be non empty doubleLoopStr, I be Ideal of L;

      :: IDEAL_1:def25

      attr I is finitely_generated means ex F be non empty finite Subset of L st I = (F -Ideal );

    end

    registration

      let L be non empty doubleLoopStr;

      cluster finitely_generated for Ideal of L;

      existence

      proof

        consider x be object such that

         A1: x in the carrier of L by XBOOLE_0:def 1;

        reconsider x as Element of L by A1;

        take ( {x} -Ideal );

        thus thesis;

      end;

    end

    registration

      let L be non empty doubleLoopStr, F be non empty finite Subset of L;

      cluster (F -Ideal ) -> finitely_generated;

      coherence ;

    end

    definition

      let L be non empty doubleLoopStr;

      :: IDEAL_1:def26

      attr L is Noetherian means

      : Def26: for I be Ideal of L holds I is finitely_generated;

    end

    registration

      cluster Euclidian Abelian add-associative right_zeroed right_complementable well-unital distributive commutative associative non degenerated for non empty doubleLoopStr;

      existence

      proof

        take INT.Ring ;

        thus thesis;

      end;

    end

    definition

      let L be non empty doubleLoopStr;

      let I be Ideal of L;

      :: IDEAL_1:def27

      attr I is principal means ex e be Element of L st I = ( {e} -Ideal );

    end

    definition

      let L be non empty doubleLoopStr;

      :: IDEAL_1:def28

      attr L is PID means for I be Ideal of L holds I is principal;

    end

    theorem :: IDEAL_1:93



     Th93: for L be non empty doubleLoopStr, F be non empty Subset of L st F <> {( 0. L)} holds ex x be Element of L st x <> ( 0. L) & x in F

    proof

      let L be non empty doubleLoopStr, F be non empty Subset of L;

      assume

       A1: F <> {( 0. L)};

      now

        assume

         A2: for x be set st x in F holds x = ( 0. L);

        for x be object holds x in F iff x = ( 0. L)

        proof

          let e be object;



           A3: ex a be object st a in F by XBOOLE_0:def 1;

          thus e in F implies e = ( 0. L) by A2;

          assume e = ( 0. L);

          hence thesis by A2, A3;

        end;

        hence contradiction by A1, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: IDEAL_1:94



     Th94: for R be add-associative left_zeroed right_zeroed right_complementable distributive well-unital Euclidian non empty doubleLoopStr holds R is PID

    proof

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

      let I be Ideal of R;

      per cases ;

        suppose

         A1: I = {( 0. R)};

        set e = ( 0. R);

        take e;

        thus thesis by A1, Th44;

      end;

        suppose I <> {( 0. R)};

        then

        consider x be Element of R such that

         A2: x <> ( 0. R) & x in I by Th93;

        set I9 = { y where y be Element of I : y <> ( 0. R) };



         A3: I9 c= the carrier of R

        proof

          let x be object;

          assume x in I9;

          then ex y be Element of I st x = y & y <> ( 0. R);

          hence thesis;

        end;

        x in I9 by A2;

        then

        reconsider I9 as non empty Subset of R by A3;

        consider f be Function of the carrier of R, NAT such that

         A4: for a,b be Element of R st b <> ( 0. R) holds ex q,r be Element of R st a = ((q * b) + r) & (r = ( 0. R) or (f . r) qua Element of NAT < (f . b) qua Element of NAT ) by INT_3:def 8;

        set K = the set of all (f . i) where i be Element of I9;

        set i = the Element of I9;



         A5: (f . i) in K;

        K c= NAT

        proof

          let x be object;

          assume x in K;

          then ex e be Element of I9 st (f . e) = x;

          hence thesis;

        end;

        then

        reconsider K as non empty Subset of NAT by A5;

        set k = ( min K);

        k in K by XXREAL_2:def 7;

        then

        consider e be Element of I9 such that

         A6: (f . e) = k;

        e in I9;

        then

         A7: ex e9 be Element of I st e9 = e & e9 <> ( 0. R);

        reconsider e as Element of R;

        take e;

        now

          let x be object;

           {e} c= I by A7, ZFMISC_1: 31;

          then

           A8: ( {e} -Ideal ) c= I by Def14;

          hereby

            assume

             A9: x in I;

            then

            reconsider x9 = x as Element of R;

            consider q,r be Element of R such that

             A10: x9 = ((q * e) + r) and

             A11: r = ( 0. R) or (f . r) qua Element of NAT < k by A4, A6, A7;

            now

              (q * e) in I by A7, Def2;

              then

               A12: ( - (q * e)) in I by Th13;

              assume

               A13: r <> ( 0. R);

              (( - (q * e)) + x9) = ((( - (q * e)) + (q * e)) + r) by A10, RLVECT_1:def 3

              .= (( 0. R) + r) by RLVECT_1: 5

              .= r by ALGSTR_1:def 2;

              then r in I by A9, A12, Def1;

              then r in I9 by A13;

              then (f . r) in K;

              hence contradiction by A11, A13, XXREAL_2:def 7;

            end;

            then

             A14: x9 = (q * e) by A10, RLVECT_1:def 4;

            e in {e} & {e} c= ( {e} -Ideal ) by Def14, TARSKI:def 1;

            hence x in ( {e} -Ideal ) by A14, Def2;

          end;

          assume x in ( {e} -Ideal );

          hence x in I by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    theorem :: IDEAL_1:95



     Th95: for L be non empty doubleLoopStr st L is PID holds L is Noetherian

    proof

      let L be non empty doubleLoopStr;

      assume

       A1: L is PID;

      let I be Ideal of L;

      I is principal by A1;

      then

      consider e be Element of L such that

       A2: I = ( {e} -Ideal );

      take {e};

      thus thesis by A2;

    end;

    registration

      cluster INT.Ring -> Noetherian;

      coherence

      proof

         INT.Ring is PID by Th94;

        hence thesis by Th95;

      end;

    end

    registration

      cluster Noetherian Abelian add-associative right_zeroed right_complementable well-unital distributive commutative associative non degenerated for non empty doubleLoopStr;

      existence

      proof

        take INT.Ring ;

        thus thesis;

      end;

    end

    theorem :: IDEAL_1:96

    for R be Noetherian add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital non empty doubleLoopStr holds for B be non empty Subset of R holds ex C be non empty finite Subset of R st C c= B & (C -Ideal ) = (B -Ideal )

    proof

      let R be Noetherian add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital non empty doubleLoopStr;

      let B be non empty Subset of R;

      defpred P[ object, object] means ex cL be non empty LinearCombination of B st $1 = ( Sum cL) & ex fsB be FinSequence of B st ( dom fsB) = ( dom cL) & $2 = ( rng fsB) & for i be Nat st i in ( dom cL) holds ex u,v be Element of R st (cL /. i) = ((u * (fsB /. i) qua Element of B qua Element of R) * v);

      (B -Ideal ) is finitely_generated by Def26;

      then

      consider D be non empty finite Subset of R such that

       A1: (D -Ideal ) = (B -Ideal );



       A2: D c= (B -Ideal ) by A1, Def14;



       A3: for e be object st e in D holds ex u be object st u in ( bool B) & P[e, u]

      proof

        let e be object;

        assume e in D;

        then

        consider cL be LinearCombination of B such that

         A4: e = ( Sum cL) by A2, Th60;

        per cases ;

          suppose

           A5: cL is non empty;

          defpred P1[ set, Element of B] means ex u,v be Element of R st (cL /. $1) = ((u * $2 qua Element of R) * v);

           A6:

          now

            let k be Nat;

            assume k in ( Seg ( len cL));

            then k in ( dom cL) by FINSEQ_1:def 3;

            then

            consider u,v be Element of R, a be Element of B such that

             A7: (cL /. k) = ((u * a) * v) by Def8;

            take d = a;

            thus P1[k, d] by A7;

          end;

          consider fsB be FinSequence of B such that

           A8: ( dom fsB) = ( Seg ( len cL)) & for k be Nat st k in ( Seg ( len cL)) holds P1[k, (fsB /. k) qua Element of B] from RECDEF_1:sch 17( A6);

          take u = ( rng fsB);

          thus u in ( bool B);

          ( dom cL) = ( Seg ( len cL)) by FINSEQ_1:def 3;

          hence thesis by A4, A5, A8;

        end;

          suppose

           A9: cL is empty;

          set b = the Element of B;

          set kL = <*((( 0. R) * b) * ( 0. R))*>;

          now

            let i be set;

            assume

             A10: i in ( dom kL);

            take u = ( 0. R), v = ( 0. R), b;

            i in ( Seg ( len kL)) by A10, FINSEQ_1:def 3;

            then i in {1} by FINSEQ_1: 2, FINSEQ_1: 40;

            then i = 1 by TARSKI:def 1;

            hence (kL /. i) = ((u * b) * v) by FINSEQ_4: 16;

          end;

          then

          reconsider kL as non empty LinearCombination of B by Def8;

          cL = ( <*> the carrier of R) by A9;



          then

           A11: e = ( 0. R) by A4, RLVECT_1: 43

          .= ((( 0. R) * b) * ( 0. R)) by BINOM: 2

          .= ( Sum kL) by BINOM: 3;

          defpred P2[ Nat, Element of B] means ex u,v be Element of R st (kL /. $1) = ((u * $2 qua Element of B qua Element of R) * v);

           A12:

          now

            let k be Nat;

            assume

             A13: k in ( Seg ( len kL));

            take b;

            k in {1} by A13, FINSEQ_1: 2, FINSEQ_1: 40;

            then k = 1 by TARSKI:def 1;

            hence P2[k, b] by FINSEQ_4: 16;

          end;

          consider fsB be FinSequence of B such that

           A14: ( dom fsB) = ( Seg ( len kL)) & for k be Nat st k in ( Seg ( len kL)) holds P2[k, (fsB /. k) qua Element of B] from RECDEF_1:sch 17( A12);

          take u = ( rng fsB);

          thus u in ( bool B);

          ( dom kL) = ( Seg ( len kL)) by FINSEQ_1:def 3;

          hence thesis by A11, A14;

        end;

      end;

      consider f be Function of D, ( bool B) such that

       A15: for e be object st e in D holds P[e, (f . e)] from FUNCT_2:sch 1( A3);

       A16:

      now

        let r be set;

        assume r in ( rng f);

        then

        consider x be object such that

         A17: x in ( dom f) & r = (f . x) by FUNCT_1:def 3;

        ex cL be non empty LinearCombination of B st x = ( Sum cL) & ex fsB be FinSequence of B st ( dom fsB) = ( dom cL) & r = ( rng fsB) & for i be Nat st i in ( dom cL) holds ex u,v be Element of R st (cL /. i) = ((u * (fsB /. i) qua Element of B qua Element of R) * v) by A15, A17;

        hence r is finite;

      end;

      reconsider rf = ( rng f) as Subset-Family of B;

      reconsider C = ( union rf) as Subset of B;

      consider r be object such that

       A18: r in ( rng f) by XBOOLE_0:def 1;

      consider x be object such that

       A19: x in ( dom f) & r = (f . x) by A18, FUNCT_1:def 3;

      reconsider r as set by TARSKI: 1;

      ex cL be non empty LinearCombination of B st x = ( Sum cL) & ex fsB be FinSequence of B st ( dom fsB) = ( dom cL) & r = ( rng fsB) & for i be Nat st i in ( dom cL) holds ex u,v be Element of R st (cL /. i) = ((u * (fsB /. i) qua Element of B qua Element of R) * v) by A15, A19;

      then r is non empty by RELAT_1: 42;

      then ex x be object st x in r;

      then

      reconsider C as non empty finite Subset of R by A18, A16, FINSET_1: 7, TARSKI:def 4, XBOOLE_1: 1;

      now

        let d be object;

        assume

         A20: d in D;

        then

        consider cL be non empty LinearCombination of B such that

         A21: d = ( Sum cL) and

         A22: ex fsB be FinSequence of B st ( dom fsB) = ( dom cL) & (f . d) = ( rng fsB) & for i be Nat st i in ( dom cL) holds ex u,v be Element of R st (cL /. i) = ((u * (fsB /. i) qua Element of B qua Element of R) * v) by A15;

        d in ( dom f) by A20, FUNCT_2:def 1;

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

        then

         A23: (f . d) c= C by ZFMISC_1: 74;

        now

          let i be set;

          consider fsB be FinSequence of B such that

           A24: ( dom fsB) = ( dom cL) and

           A25: (f . d) = ( rng fsB) and

           A26: for i be Nat st i in ( dom cL) holds ex u,v be Element of R st (cL /. i) = ((u * (fsB /. i) qua Element of B qua Element of R) * v) by A22;

          assume

           A27: i in ( dom cL);

          then (fsB /. i) = (fsB . i) by A24, PARTFUN1:def 6;

          then

           A28: (fsB /. i) in (f . d) by A27, A24, A25, FUNCT_1:def 3;

          ex u,v be Element of R st (cL /. i) = ((u * (fsB /. i) qua Element of B qua Element of R) * v) by A27, A26;

          hence ex u,v be Element of R, a be Element of C st (cL /. i) = ((u * a) * v) by A23, A28;

        end;

        then

        reconsider cL9 = cL as LinearCombination of C by Def8;

        d = ( Sum cL9) by A21;

        hence d in (C -Ideal ) by Th60;

      end;

      then D c= (C -Ideal );

      then (D -Ideal ) c= ((C -Ideal ) -Ideal ) by Th57;

      then

       A29: (B -Ideal ) c= (C -Ideal ) by A1, Th44;

      take C;

      (C -Ideal ) c= (B -Ideal ) by Th57;

      hence thesis by A29;

    end;

    theorem :: IDEAL_1:97

    for R be non empty doubleLoopStr st for B be non empty Subset of R holds ex C be non empty finite Subset of R st C c= B & (C -Ideal ) = (B -Ideal ) holds for a be sequence of R holds ex m be Element of NAT st (a . (m + 1)) in (( rng (a | (m + 1))) -Ideal )

    proof

      let R be non empty doubleLoopStr;

      assume

       A1: for B be non empty Subset of R holds ex C be non empty finite Subset of R st C c= B & (C -Ideal ) = (B -Ideal );

      let a be sequence of R;

      reconsider B = ( rng a) as non empty Subset of R;

      consider C be non empty finite Subset of R such that

       A2: C c= B and

       A3: (C -Ideal ) = (B -Ideal ) by A1;

      defpred P[ object, object] means $1 = (a . $2);



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



       A5: for e be object st e in C holds ex u be object st u in NAT & P[e, u]

      proof

        let e be object;

        assume e in C;

        then

        consider u be object such that

         A6: u in ( dom a) and

         A7: e = (a . u) by A2, FUNCT_1:def 3;

        take u;

        thus u in NAT by A6;

        thus thesis by A7;

      end;

      consider f be Function of C, NAT such that

       A8: for e be object st e in C holds P[e, (f . e)] from FUNCT_2:sch 1( A5);

      set Rf = ( rng f);

      reconsider Rf as non empty finite Subset of NAT ;

      reconsider m = ( max Rf) as Element of NAT by ORDINAL1:def 12;

      set D = ( rng (a | ( Segm (m + 1))));



       A9: ( dom f) = C by FUNCT_2:def 1;



       A10: C c= D

      proof

        let X be object;

        set fx = (f . X);

        assume

         A11: X in C;

        then (f . X) in Rf by A9, FUNCT_1:def 3;

        then fx <= m by XXREAL_2:def 8;

        then fx < (m + 1) by NAT_1: 13;

        then fx in ( Segm (m + 1)) by NAT_1: 44;

        then (a . fx) in ( rng (a | ( Segm (m + 1)))) by A4, FUNCT_1: 50;

        hence thesis by A8, A11;

      end;

      then

      reconsider D as non empty Subset of R;



       A12: (D -Ideal ) c= (B -Ideal ) by Th57, RELAT_1: 70;

      (B -Ideal ) c= (D -Ideal ) by A3, A10, Th57;

      then

       A13: (D -Ideal ) = (B -Ideal ) by A12;

      take m;

      B c= (B -Ideal ) & (a . (m + 1)) in B by Def14, FUNCT_2: 4;

      hence thesis by A13;

    end;

    registration

      let X,Y be non empty set, f be Function of X, Y, A be non empty Subset of X;

      cluster (f | A) -> non empty;

      coherence

      proof

        ( dom f) = X by FUNCT_2:def 1;

        then (( dom f) /\ A) is non empty by XBOOLE_1: 28;

        then ( dom f) meets A;

        hence thesis by RELAT_1: 66;

      end;

    end

    theorem :: IDEAL_1:98

    for R be non empty doubleLoopStr st for a be sequence of R holds ex m be Element of NAT st (a . (m + 1)) in (( rng (a | (m + 1))) -Ideal ) holds not ex F be sequence of ( bool the carrier of R) st (for i be Nat holds (F . i) is Ideal of R) & (for j,k be Nat st j < k holds (F . j) c< (F . k))

    proof

      let R be non empty doubleLoopStr;

      assume

       A1: for a be sequence of R holds ex m be Element of NAT st (a . (m + 1)) in (( rng (a | (m + 1))) -Ideal );

      given F be sequence of ( bool the carrier of R) such that

       A2: for i be Nat holds (F . i) is Ideal of R and

       A3: for j,k be Nat st j < k holds (F . j) c< (F . k);

      defpred P[ object, object] means ex n be Element of NAT st n = $1 & (n = 0 implies $2 in (F . 0 )) & (n > 0 implies ex k be Element of NAT st n = (k + 1) & $2 in ((F . n) \ (F . k)));



       A4: for e be object st e in NAT holds ex u be object st u in the carrier of R & P[e, u]

      proof

        let e be object;

        assume e in NAT ;

        then

        reconsider n = e as Element of NAT ;

        per cases ;

          suppose

           A5: n = 0 ;

          (F . 0 ) is Ideal of R by A2;

          then

          consider u be object such that

           A6: u in (F . 0 ) by XBOOLE_0:def 1;

          take u;

          thus u in the carrier of R by A6;

          take n;

          thus n = e;

          thus thesis by A5, A6;

        end;

          suppose n > 0 ;

          then

          consider k be Nat such that

           A7: n = (k + 1) by NAT_1: 6;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          n > k by A7, NAT_1: 13;

          then not (F . n) c= (F . k) by A3, XBOOLE_1: 60;

          then ((F . n) \ (F . k)) is non empty by XBOOLE_1: 37;

          then

          consider u be object such that

           A8: u in ((F . n) \ (F . k));

          take u;

          thus u in the carrier of R by A8;

          take n;

          thus n = e;

          thus thesis by A7, A8;

        end;

      end;

      consider f be sequence of the carrier of R such that

       A9: for e be object st e in NAT holds P[e, (f . e)] from FUNCT_2:sch 1( A4);

      consider m be Element of NAT such that

       A10: (f . (m + 1)) in (( rng (f | (m + 1))) -Ideal ) by A1;

      reconsider m1 = (m + 1) as non zero Nat;



       A11: ex n be Element of NAT st n = (m + 1) & (n = 0 implies (f . (m + 1)) in (F . 0 )) & (n > 0 implies ex k be Element of NAT st n = (k + 1) & (f . (m + 1)) in ((F . n) \ (F . k))) by A9;

      defpred P[ Nat] means ( rng (f | ( Segm ($1 + 1)))) c= (F . $1);



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

      proof

        let k be Nat such that

         A13: ( rng (f | ( Segm (k + 1)))) c= (F . k);

        let y be object;

        assume y in ( rng (f | ( Segm ((k + 1) + 1))));

        then

        consider x be object such that

         A14: x in ( dom (f | ( Segm ((k + 1) + 1)))) and

         A15: y = ((f | ( Segm ((k + 1) + 1))) . x) by FUNCT_1:def 3;



         A16: x in ( dom f) by A14, RELAT_1: 57;

        reconsider nx = x as Element of NAT by A14;

        x in ( Segm ((k + 1) + 1)) by A14, RELAT_1: 57;

        then nx < ((k + 1) + 1) by NAT_1: 44;

        then

         A17: nx <= (k + 1) by NAT_1: 13;

        per cases by A17, XXREAL_0: 1;

          suppose nx < (k + 1);

          then

           A18: nx in ( Segm (k + 1)) by NAT_1: 44;

          k < (k + 1) by NAT_1: 13;

          then (F . k) c< (F . (k + 1)) by A3;

          then

           A19: (F . k) c= (F . (k + 1));

          y = (f . nx) by A14, A15, FUNCT_1: 47;

          then y in ( rng (f | ( Segm (k + 1)))) by A16, A18, FUNCT_1: 50;

          then y in (F . k) by A13;

          hence thesis by A19;

        end;

          suppose

           A20: nx = (k + 1);

          y = (f . nx) & ex n be Element of NAT st n = nx & (n = 0 implies (f . nx) in (F . 0 )) & (n > 0 implies ex k be Element of NAT st n = (k + 1) & (f . nx) in ((F . n) \ (F . k))) by A9, A14, A15, FUNCT_1: 47;

          hence thesis by A20, XBOOLE_0:def 5;

        end;

      end;

      (F . m) is Ideal of R by A2;

      then

       A21: (F . m) = ((F . m) -Ideal ) by Th44;



       A22: P[ 0 ]

      proof

        let y be object;

        assume y in ( rng (f | ( Segm ( 0 + 1))));

        then

        consider x be object such that

         A23: x in ( dom (f | ( Segm 1))) and

         A24: y = ((f | ( Segm 1)) . x) by FUNCT_1:def 3;

        x in ( Segm 1) & ex n be Element of NAT st n = x & (n = 0 implies (f . x) in (F . 0 )) & (n > 0 implies ex k be Element of NAT st n = (k + 1) & (f . x) in ((F . n) \ (F . k))) by A9, A23, RELAT_1: 57;

        hence thesis by A24, CARD_1: 49, FUNCT_1: 49, TARSKI:def 1;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A22, A12);

      then (( rng (f | ( Segm m1))) -Ideal ) c= (F . m) by A21, Th57;

      hence contradiction by A10, A11, XBOOLE_0:def 5;

    end;

    theorem :: IDEAL_1:99

    for R be non empty doubleLoopStr st not ex F be sequence of ( bool the carrier of R) st (for i be Element of NAT holds (F . i) is Ideal of R) & (for j,k be Element of NAT st j < k holds (F . j) c< (F . k)) holds R is Noetherian

    proof

      let R be non empty doubleLoopStr such that

       A1: not ex F be sequence of ( bool the carrier of R) st (for i be Element of NAT holds (F . i) is Ideal of R) & (for j,k be Element of NAT st j < k holds (F . j) c< (F . k)) and

       A2: not R is Noetherian;

      consider I be Ideal of R such that

       A3: not I is finitely_generated by A2;

      set D = { S where S be Subset of R : S is non empty finite Subset of I };

      consider e be object such that

       A4: e in I by XBOOLE_0:def 1;

      reconsider e as Element of R by A4;

       {e} c= I by A4, ZFMISC_1: 31;

      then

       A5: {e} in D;

      D c= ( bool the carrier of R)

      proof

        let x be object;

        assume x in D;

        then ex s be Subset of R st x = s & s is non empty finite Subset of I;

        hence thesis;

      end;

      then

      reconsider D as non empty Subset-Family of R by A5;

      reconsider e9 = {e} as Element of D by A5;

      defpred P[ set, Element of D, set] means ex r be Element of R st r in (I \ ($2 -Ideal )) & $3 = ($2 \/ {r});



       A6: for n be Nat holds for x be Element of D holds ex y be Element of D st P[n, x, y]

      proof

        let n be Nat, x be Element of D;

        x in D;

        then

        consider x9 be Subset of R such that

         A7: x9 = x and

         A8: x9 is non empty finite Subset of I;

        reconsider x19 = x9 as non empty finite Subset of I by A8;

        (x9 -Ideal ) c= (I -Ideal ) by A8, Th57;

        then (x9 -Ideal ) c= I by Th44;

        then not I c= (x9 -Ideal ) by A3, A8, XBOOLE_0:def 10;

        then

        consider r be object such that

         A9: r in I and

         A10: not r in (x9 -Ideal );

        set y = (x19 \/ {r});



         A11: y c= I

        proof

          let x be object;

          assume x in y;

          then x in x19 or x in {r} by XBOOLE_0:def 3;

          hence thesis by A9, TARSKI:def 1;

        end;

        then y is Subset of R by XBOOLE_1: 1;

        then

         A12: y in D by A11;

        reconsider r as Element of R by A9;

        reconsider y as Element of D by A12;

        take y;

        take r;

        thus thesis by A7, A9, A10, XBOOLE_0:def 5;

      end;

      consider f be sequence of D such that

       A13: (f . 0 ) = e9 & for n be Nat holds P[n, (f . n) qua Element of D, (f . (n + 1))] from RECDEF_1:sch 2( A6);

      defpred Q[ Nat, Subset of R] means ex c be Subset of R st c = (f . $1) & $2 = (c -Ideal );



       A14: for x be Element of NAT holds ex y be Subset of R st Q[x, y]

      proof

        let x be Element of NAT ;

        (f . x) in D;

        then

        consider c be Subset of R such that

         A15: c = (f . x) and c is non empty finite Subset of I;

        reconsider y = (c -Ideal ) as Subset of R;

        take y;

        take c;

        thus thesis by A15;

      end;

      consider F be sequence of ( bool the carrier of R) such that

       A16: for x be Element of NAT holds Q[x, (F . x)] from FUNCT_2:sch 3( A14);



       A17: for x be Nat holds Q[x, (F . x)]

      proof

        let x be Nat;

        x in NAT by ORDINAL1:def 12;

        hence thesis by A16;

      end;



       A18: for j,k be Element of NAT st j < k holds (F . j) c< (F . k)

      proof

        let j,k be Element of NAT ;

        defpred P[ Nat] means (F . j) c< (F . ((j + 1) + $1));

        assume j < k;

        then (j + 1) <= k by NAT_1: 13;

        then

        consider i be Nat such that

         A19: k = ((j + 1) + i) by NAT_1: 10;



         A20: for i be Nat holds (F . i) c< (F . (i + 1))

        proof

          let i be Nat;

          consider c be Subset of R such that

           A21: c = (f . i) and

           A22: (F . i) = (c -Ideal ) by A17;

          consider c1 be Subset of R such that

           A23: c1 = (f . (i + 1)) and

           A24: (F . (i + 1)) = (c1 -Ideal ) by A17;



           A25: c1 c= (c1 -Ideal ) by Def14;

          consider r be Element of R such that

           A26: r in (I \ (c -Ideal )) and

           A27: c1 = (c \/ {r}) by A13, A21, A23;

          c in D by A21;

          then ex c9 be Subset of R st c9 = c & c9 is non empty finite Subset of I;

          hence (F . i) c= (F . (i + 1)) by A22, A24, A27, Th57, XBOOLE_1: 7;

          r in {r} by TARSKI:def 1;

          then r in c1 by A27, XBOOLE_0:def 3;

          hence thesis by A22, A24, A26, A25, XBOOLE_0:def 5;

        end;



         A28: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat such that

           A29: (F . j) c= (F . ((j + 1) + i)) and (F . j) <> (F . ((j + 1) + i));



           A30: (F . ((j + 1) + i)) c< (F . (((j + 1) + i) + 1)) by A20;

          then (F . ((j + 1) + i)) c= (F . (((j + 1) + i) + 1));

          hence (F . j) c= (F . ((j + 1) + (i + 1))) by A29;

          thus thesis by A29, A30, XBOOLE_0:def 8;

        end;



         A31: P[ 0 ] by A20;



         A32: for i be Nat holds P[i] from NAT_1:sch 2( A31, A28);

        thus thesis by A32, A19;

      end;

      for i be Element of NAT holds (F . i) is Ideal of R

      proof

        let i be Element of NAT ;

        ex c be Subset of R st c = (f . i) & (F . i) = (c -Ideal ) by A17;

        hence thesis;

      end;

      hence contradiction by A1, A18;

    end;