realalg1.miz



    begin

    definition

      let X be set;

      let R be Relation of X;

      :: REALALG1:def1

      attr R is strongly_reflexive means

      : defstr: R is_reflexive_in X;

      :: REALALG1:def2

      attr R is totally_connected means

      : Rtot: R is_strongly_connected_in X;

    end

    registration

      let X be set;

      cluster strongly_reflexive for Relation of X;

      existence

      proof

        per cases ;

          suppose

           AS: X is empty;

          reconsider R = {} as Relation of X, X by RELSET_1: 12;

          take R;

          for o be object st o in X holds [o, o] in R by AS;

          hence R is strongly_reflexive by RELAT_2:def 1;

        end;

          suppose

           AS: X is non empty;

          set R = the set of all [x, y] where x,y be Element of X;

          now

            let o be object;

            assume o in R;

            then

            consider x,y be Element of X such that

             A: o = [x, y];

            thus o in [:X, X:] by AS, A, ZFMISC_1:def 2;

          end;

          then

          reconsider R as Relation of X by TARSKI:def 3;

          take R;

          for o be object st o in X holds [o, o] in R;

          hence R is strongly_reflexive by RELAT_2:def 1;

        end;

      end;

      cluster totally_connected for Relation of X;

      existence

      proof

        per cases ;

          suppose

           AS: X is empty;

          reconsider R = {} as Relation of X, X by RELSET_1: 12;

          take R;

          for x,y be object st x in X & y in X holds [x, y] in R or [y, x] in R by AS;

          hence R is totally_connected by RELAT_2:def 7;

        end;

          suppose

           AS: X is non empty;

          set R = the set of all [x, y] where x,y be Element of X;

          now

            let o be object;

            assume o in R;

            then

            consider x,y be Element of X such that

             A: o = [x, y];

            thus o in [:X, X:] by AS, A, ZFMISC_1:def 2;

          end;

          then

          reconsider R as Relation of X by TARSKI:def 3;

          take R;

          for x,y be object st x in X & y in X holds [x, y] in R or [y, x] in R;

          hence R is totally_connected by RELAT_2:def 7;

        end;

      end;

    end

    registration

      let X be set;

      cluster strongly_reflexive -> reflexive for Relation of X;

      coherence

      proof

        let R be Relation of X;

        assume

         AS: R is strongly_reflexive;

        

         H: ( field R) c= (X \/ X) by RELSET_1: 8;

        now

          let o be object;

          assume

           A: o in ( field R);

          then

          reconsider x = o as Element of X by H;

          per cases ;

            suppose X is empty;

            hence [o, o] in R by H, A;

          end;

            suppose X is non empty;

            then x in X;

            hence [o, o] in R by AS, RELAT_2:def 1;

          end;

        end;

        hence R is reflexive by RELAT_2:def 9, RELAT_2:def 1;

      end;

      cluster totally_connected -> strongly_connected for Relation of X;

      coherence

      proof

        let R be Relation of X;

        assume

         AS: R is totally_connected;

        

         H: ( field R) c= (X \/ X) by RELSET_1: 8;

        now

          let o1,o2 be object;

          assume

           A: o1 in ( field R) & o2 in ( field R);

          then

          reconsider x = o1, y = o2 as Element of X by H;

          per cases ;

            suppose X is empty;

            hence [o1, o2] in R or [o2, o1] in R by H, A;

          end;

            suppose X is non empty;

            then [x, y] in R or [y, x] in R by AS, RELAT_2:def 7;

            hence [o1, o2] in R or [o2, o1] in R;

          end;

        end;

        hence R is strongly_connected by RELAT_2:def 15, RELAT_2:def 7;

      end;

    end

    registration

      let X be non empty set;

      cluster strongly_reflexive -> non empty for Relation of X;

      coherence

      proof

        let R be Relation of X;

        assume

         AS: R is strongly_reflexive;

        set x = the Element of X;

         [x, x] in R by AS, RELAT_2:def 1;

        hence thesis;

      end;

      cluster totally_connected -> non empty for Relation of X;

      coherence

      proof

        let R be Relation of X;

        assume R is totally_connected;

        then for x,y be Element of X holds [x, y] in R or [y, x] in R by RELAT_2:def 7;

        hence thesis;

      end;

    end

    theorem :: REALALG1:1

    for X be non empty set holds for R be strongly_reflexive Relation of X holds for x be Element of X holds x <=_ (R,x) by defstr, RELAT_2:def 1;

    theorem :: REALALG1:2

    

     lemanti: for X be non empty set holds for R be antisymmetric Relation of X holds for x,y be Element of X st x <=_ (R,y) & y <=_ (R,x) holds x = y

    proof

      let X be non empty set;

      let R be antisymmetric Relation of X;

      let x,y be Element of X;

      assume

       A: x <=_ (R,y) & y <=_ (R,x);

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      hence x = y by A, RELAT_2:def 4, RELAT_2:def 12;

    end;

    theorem :: REALALG1:3

    

     lemtrans: for X be non empty set holds for R be transitive Relation of X holds for x,y,z be Element of X st x <=_ (R,y) & y <=_ (R,z) holds x <=_ (R,z)

    proof

      let X be non empty set;

      let R be transitive Relation of X;

      let x,y,z be Element of X;

      assume

       A: x <=_ (R,y) & y <=_ (R,z);

      then x in ( field R) & y in ( field R) & z in ( field R) by RELAT_1: 15;

      hence thesis by A, RELAT_2:def 8, RELAT_2:def 16;

    end;

    theorem :: REALALG1:4

    for X be non empty set holds for R be totally_connected Relation of X holds for x,y be Element of X holds x <=_ (R,y) or y <=_ (R,x) by Rtot, RELAT_2:def 7;

    definition

      let L be addLoopStr;

      let R be Relation of L;

      :: REALALG1:def3

      attr R is respecting_addition means

      : respadd: for a,b,c be Element of L st a <=_ (R,b) holds (a + c) <=_ (R,(b + c));

    end

    definition

      let L be multLoopStr_0;

      let R be Relation of L;

      :: REALALG1:def4

      attr R is respecting_multiplication means

      : respmult: for a,b,c be Element of L st a <=_ (R,b) & ( 0. L) <=_ (R,c) holds (a * c) <=_ (R,(b * c));

    end

    begin

    

     lemmul: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for p,q be Polynomial of L st p <> ( 0_. L) & q <> ( 0_. L) holds ((p *' q) . (((( len p) + ( len q)) - 1) -' 1)) = ((p . (( len p) -' 1)) * (q . (( len q) -' 1)))

    proof

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

      let p,q be Polynomial of L;

      assume p <> ( 0_. L) & q <> ( 0_. L);

      then

       B: ( len p) >= 1 & ( len q) >= 1 by NAT_1: 14, POLYNOM4: 5;

      then (( len p) + ( len q)) >= (1 + 1) by XREAL_1: 7;

      then

       A: ((( len p) + ( len q)) - 1) >= ((1 + 1) - 1) by XREAL_1: 9;

      reconsider j = ((( len p) + ( len q)) - 1) as Element of NAT by B, INT_1: 3;

      set i = (j -' 1);

      consider r be FinSequence of the carrier of L such that

       M: ( len r) = (i + 1) & ((p *' q) . i) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by POLYNOM3:def 9;

      

       A7: (j - 1) = i by A, XREAL_0:def 2;

      reconsider x = (( len q) - 1) as Element of NAT by B, INT_1: 3;

      

       A3: j = (( len p) + x);

      then j >= ( len p) by NAT_1: 11;

      then

       A1: ( len p) in ( dom r) by A7, M, B, FINSEQ_3: 25;

      

       A2: ((i + 1) -' ( len p)) = (((((( len p) + ( len q)) - 1) - 1) + 1) - ( len p)) by A3, A7, XREAL_0:def 2

      .= (((( len p) - ( len p)) + ( len q)) - 1)

      .= (( len q) -' 1) by B, XREAL_0:def 2;

      now

        let k be Element of NAT ;

        assume

         E: k in ( dom r) & k <> ( len p);

        per cases by E, XXREAL_0: 1;

          suppose

           E1: k > ( len p);

          then

          reconsider k1 = (k - 1) as Element of NAT by INT_1: 3;

          

           E2: (k1 + 1) > ( len p) by E1;

          (k -' 1) = (k - 1) by E1, XREAL_0:def 2;

          then (p . (k -' 1)) = ( 0. L) by E2, ALGSEQ_1: 8, NAT_1: 13;

          then (r . k) = (( 0. L) * (q . ((i + 1) -' k))) by E, M;

          hence (r /. k) = ( 0. L) by E, PARTFUN1:def 6;

        end;

          suppose k < ( len p);

          then (k + 1) <= ( len p) by INT_1: 7;

          then ((k + 1) - k) <= (( len p) - k) by XREAL_1: 9;

          then ((( len p) - k) + ( len q)) >= (1 + ( len q)) by XREAL_1: 6;

          then

           E2: (((( len p) - k) + ( len q)) - 1) >= ((( len q) + 1) - 1) by XREAL_1: 9;

          ((i + 1) - k) = (((((( len p) + ( len q)) - 1) - 1) + 1) - k) by A, XREAL_0:def 2;

          then ((i + 1) -' k) = (((( len p) + ( len q)) - 1) - k) by E2, XREAL_0:def 2;

          then (q . ((i + 1) -' k)) = ( 0. L) by E2, ALGSEQ_1: 8;

          then (r . k) = ((p . (k -' 1)) * ( 0. L)) by E, M;

          hence (r /. k) = ( 0. L) by E, PARTFUN1:def 6;

        end;

      end;

      

      then ( Sum r) = (r /. ( len p)) by A1, POLYNOM2: 3

      .= (r . ( len p)) by A1, PARTFUN1:def 6

      .= ((p . (( len p) -' 1)) * (q . ((i + 1) -' ( len p)))) by A1, M;

      hence thesis by M, A2;

    end;

    theorem :: REALALG1:5

    for R be degenerated Ring, p be Polynomial of R holds { i where i be Nat : (p . i) <> ( 0. R) } = {}

    proof

      let R be degenerated Ring, p be Polynomial of R;

       A:

      now

        let i be Nat;

        

        thus (p . i) = ((p . i) * ( 1. R))

        .= ((p . i) * ( 0. R)) by STRUCT_0:def 8

        .= ( 0. R);

      end;

      set M = { i where i be Nat : (p . i) <> ( 0. R) };

      now

        assume

         B: M <> {} ;

        let x be Element of M;

        x in M by B;

        then

        consider j be Nat such that

         H1: j = x & (p . j) <> ( 0. R);

        thus contradiction by H1, A;

      end;

      hence thesis;

    end;

    theorem :: REALALG1:6

    

     lemlp0: for R be Ring, p be Polynomial of R holds p = ( 0_. R) iff { i where i be Nat : (p . i) <> ( 0. R) } = {}

    proof

      let R be Ring, p be Polynomial of R;

      hereby

        assume

         AS: p = ( 0_. R);

        now

          assume { i where i be Nat : (p . i) <> ( 0. R) } is non empty;

          then

          consider x be object such that

           H1: x in { i where i be Nat : (p . i) <> ( 0. R) };

          consider i be Nat such that

           H2: x = i & (p . i) <> ( 0. R) by H1;

          thus contradiction by AS, H2, FUNCOP_1: 7, ORDINAL1:def 12;

        end;

        hence { i where i be Nat : (p . i) <> ( 0. R) } = {} ;

      end;

      assume

       AS: { i where i be Nat : (p . i) <> ( 0. R) } = {} ;

      assume p <> ( 0_. R);

      then ( len p) <> 0 by POLYNOM4: 5;

      then (( len p) + 1) > ( 0 + 1) by XREAL_1: 6;

      then ( len p) >= 1 by NAT_1: 13;

      then

      reconsider k = (( len p) - 1) as Element of NAT by INT_1: 3;

      reconsider k as Nat;

      ( len p) = (k + 1);

      then (p . k) <> ( 0. R) by ALGSEQ_1: 10;

      then k in { i where i be Nat : (p . i) <> ( 0. R) };

      hence contradiction by AS;

    end;

    theorem :: REALALG1:7

    

     lemlowp0: for R be Ring, p be Polynomial of R holds ( min* { i where i be Nat : ((p + ( 0_. R)) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (p . i) <> ( 0. R) })

    proof

      let R be Ring, p be Polynomial of R;

      now

        let o be object;

        assume o in { i where i be Nat : (p . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H1: o = i & (p . i) <> ( 0. R);

        thus o in NAT by H1, ORDINAL1:def 12;

      end;

      then

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) } as Subset of NAT by TARSKI:def 3;

      now

        let o be object;

        assume o in { i where i be Nat : ((p + ( 0_. R)) . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H1: o = i & ((p + ( 0_. R)) . i) <> ( 0. R);

        thus o in NAT by H1, ORDINAL1:def 12;

      end;

      then

      reconsider cpq = { i where i be Nat : ((p + ( 0_. R)) . i) <> ( 0. R) } as Subset of NAT by TARSKI:def 3;

      per cases ;

        suppose cp is non empty;

        then ( min* cp) in cp by NAT_1:def 1;

        then

        consider i be Nat such that

         H1: ( min* cp) = i & (p . i) <> ( 0. R);

        ((p + ( 0_. R)) . i) = ((p . i) + (( 0_. R) . i)) by NORMSP_1:def 2

        .= ((p . i) + ( 0. R)) by ORDINAL1:def 12, FUNCOP_1: 7

        .= (p . i);

        then

         B: ( min* cp) in cpq by H1;

        now

          let k be Nat;

          assume k in cpq;

          then

          consider i be Nat such that

           C1: k = i & ((p + ( 0_. R)) . i) <> ( 0. R);

          now

            assume ( min* cp) > k;

            then

             C2: not (k in cp) by NAT_1:def 1;

            ((p + ( 0_. R)) . k) = ((p . k) + (( 0_. R) . k)) by NORMSP_1:def 2

            .= ((p . k) + ( 0. R)) by ORDINAL1:def 12, FUNCOP_1: 7

            .= ( 0. R) by C2;

            hence contradiction by C1;

          end;

          hence ( min* cp) <= k;

        end;

        hence ( min* { i where i be Nat : ((p + ( 0_. R)) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (p . i) <> ( 0. R) }) by B, NAT_1:def 1;

      end;

        suppose

         A: cp is empty;

        then p = ( 0_. R) by lemlp0;

        hence ( min* { i where i be Nat : ((p + ( 0_. R)) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (p . i) <> ( 0. R) }) by A, lemlp0, POLYNOM3: 28;

      end;

    end;

    

     lemlp1: for R be non degenerated Ring, p be non zero Polynomial of R holds { i where i be Nat : (p . i) <> ( 0. R) } is non empty Subset of NAT

    proof

      let R be non degenerated Ring, p be non zero Polynomial of R;

       A:

      now

        let o be object;

        assume o in { i where i be Nat : (p . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H: o = i & (p . i) <> ( 0. R);

        thus o in NAT by H, ORDINAL1:def 12;

      end;

      p <> ( 0_. R);

      hence thesis by A, lemlp0, TARSKI:def 3;

    end;

    theorem :: REALALG1:8

    

     lemlowp2: for R be non degenerated Ring, p be Polynomial of R holds ( min* { i where i be Nat : (( - p) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (p . i) <> ( 0. R) })

    proof

      let R be non degenerated Ring, p be Polynomial of R;

      per cases ;

        suppose p = ( 0_. R);

        then ( - p) = p by HURWITZ: 9;

        hence thesis;

      end;

        suppose p <> ( 0_. R);

        then

        reconsider pp = p as non zero Polynomial of R by UPROOTS:def 5;

        reconsider cp = { i where i be Nat : (pp . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

        ( min* cp) in cp by NAT_1:def 1;

        then

        consider j be Nat such that

         A0: j = ( min* cp) & (p . j) <> ( 0. R);

        now

          assume (( - p) . j) = ( 0. R);

          then

           A1: ( 0. R) = ( - (p . j)) by BHSP_1: 44;

          (p . j) = ( - ( - (p . j)))

          .= ( 0. R) by A1;

          hence contradiction by A0;

        end;

        then

         A: j in { i where i be Nat : (( - p) . i) <> ( 0. R) };

        now

          let o be object;

          assume o in { i where i be Nat : (( - p) . i) <> ( 0. R) };

          then

          consider i be Nat such that

           H1: o = i & (( - p) . i) <> ( 0. R);

          thus o in NAT by H1, ORDINAL1:def 12;

        end;

        then

        reconsider cmp = { i where i be Nat : (( - p) . i) <> ( 0. R) } as non empty Subset of NAT by A, TARSKI:def 3;

        now

          let k be Nat;

          assume k in { i where i be Nat : (( - p) . i) <> ( 0. R) };

          then

          consider i be Nat such that

           A3: k = i & (( - p) . i) <> ( 0. R);

          now

            assume (p . i) = ( 0. R);

            then ( - (p . i)) = ( 0. R);

            hence (( - p) . i) = ( 0. R) by BHSP_1: 44;

          end;

          then i in cp by A3;

          hence j <= k by A3, A0, NAT_1:def 1;

        end;

        then j = ( min* cmp) by A, NAT_1:def 1;

        hence thesis by A0;

      end;

    end;

    theorem :: REALALG1:9

    

     lemlowp1a1: for R be non degenerated Ring, p,q be non zero Polynomial of R st ( min* { i where i be Nat : (p . i) <> ( 0. R) }) > ( min* { i where i be Nat : (q . i) <> ( 0. R) }) holds ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (q . i) <> ( 0. R) })

    proof

      let R be non degenerated Ring;

      let p,q be non zero Polynomial of R;

      assume

       AS1: ( min* { i where i be Nat : (p . i) <> ( 0. R) }) > ( min* { i where i be Nat : (q . i) <> ( 0. R) });

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      now

        let o be object;

        assume o in { i where i be Nat : ((p + q) . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H1: o = i & ((p + q) . i) <> ( 0. R);

        thus o in NAT by H1, ORDINAL1:def 12;

      end;

      then

      reconsider cpq = { i where i be Nat : ((p + q) . i) <> ( 0. R) } as Subset of NAT by TARSKI:def 3;

       not (( min* cq) in cp) by AS1, NAT_1:def 1;

      then (p . ( min* cq)) = ( 0. R);

      then

       A: ((p + q) . ( min* cq)) = (( 0. R) + (q . ( min* cq))) by NORMSP_1:def 2;

      ( min* cq) in cq by NAT_1:def 1;

      then

      consider u be Nat such that

       H1: u = ( min* cq) & (q . u) <> ( 0. R);

      

       B: ( min* cq) in cpq by A, H1;

      then

      reconsider cpq as non empty Subset of NAT ;

      now

        let k be Nat;

        assume k in cpq;

        then

        consider v be Nat such that

         H2: v = k & ((p + q) . v) <> ( 0. R);

        now

          let j be Nat;

          assume

           D0: j < ( min* cq);

           D1:

          now

            assume (q . j) <> ( 0. R);

            then j in cq;

            hence contradiction by D0, NAT_1:def 1;

          end;

          now

            assume (p . j) <> ( 0. R);

            then j in cp;

            then j >= ( min* cp) by NAT_1:def 1;

            hence contradiction by D0, AS1, XXREAL_0: 2;

          end;

          

          hence ((p + q) . j) = (( 0. R) + (q . j)) by NORMSP_1:def 2

          .= ( 0. R) by D1;

        end;

        hence ( min* cq) <= k by H2;

      end;

      hence thesis by B, NAT_1:def 1;

    end;

    theorem :: REALALG1:10

    

     lemlowp1a2: for R be non degenerated Ring, p,q be non zero Polynomial of R st (p + q) <> ( 0_. R) & ( min* { i where i be Nat : (p . i) <> ( 0. R) }) = ( min* { i where i be Nat : (q . i) <> ( 0. R) }) holds ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) }) >= ( min* { i where i be Nat : (p . i) <> ( 0. R) })

    proof

      let R be non degenerated Ring, p,q be non zero Polynomial of R;

      assume

       XX: (p + q) <> ( 0_. R) & ( min* { i where i be Nat : (p . i) <> ( 0. R) }) = ( min* { i where i be Nat : (q . i) <> ( 0. R) });

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      now

        let o be object;

        assume o in { i where i be Nat : ((p + q) . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H1: o = i & ((p + q) . i) <> ( 0. R);

        thus o in NAT by H1, ORDINAL1:def 12;

      end;

      then

      reconsider cpq = { i where i be Nat : ((p + q) . i) <> ( 0. R) } as non empty Subset of NAT by lemlp0, XX, TARSKI:def 3;

      ( min* cpq) in cpq by NAT_1:def 1;

      then

      consider u be Nat such that

       H1: u = ( min* cpq) & ((p + q) . u) <> ( 0. R);

      now

        let j be Nat;

        assume

         D0: j < ( min* cp);

         D1a:

        now

          assume (p . j) <> ( 0. R);

          then j in cp;

          hence contradiction by D0, NAT_1:def 1;

        end;

        now

          assume (q . j) <> ( 0. R);

          then j in cq;

          hence contradiction by XX, D0, NAT_1:def 1;

        end;

        

        hence ((p + q) . j) = ((p . j) + ( 0. R)) by NORMSP_1:def 2

        .= ( 0. R) by D1a;

      end;

      hence thesis by H1;

    end;

    theorem :: REALALG1:11

    

     lemlowp1b: for R be non degenerated Ring, p,q be non zero Polynomial of R st ((p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) + (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) }))) <> ( 0. R) holds ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) }) = ( min (( min* { i where i be Nat : (p . i) <> ( 0. R) }),( min* { i where i be Nat : (q . i) <> ( 0. R) })))

    proof

      let R be non degenerated Ring, p,q be non zero Polynomial of R;

      assume

       XX: ((p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) + (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) }))) <> ( 0. R);

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      now

        let o be object;

        assume o in { i where i be Nat : ((p + q) . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H1: o = i & ((p + q) . i) <> ( 0. R);

        thus o in NAT by H1, ORDINAL1:def 12;

      end;

      then

      reconsider cpq = { i where i be Nat : ((p + q) . i) <> ( 0. R) } as Subset of NAT by TARSKI:def 3;

      per cases by XXREAL_0: 1;

        suppose

         A: ( min* cp) > ( min* cq);

        then ( min* cpq) = ( min* cq) by lemlowp1a1;

        hence thesis by A, XXREAL_0:def 9;

      end;

        suppose

         A: ( min* cp) < ( min* cq);

        then ( min* cpq) = ( min* cp) by lemlowp1a1;

        hence thesis by A, XXREAL_0:def 9;

      end;

        suppose

         A: ( min* cp) = ( min* cq);

        then ((p + q) . ( min* cp)) <> ( 0. R) by XX, NORMSP_1:def 2;

        then

         D1: ( min* cp) in cpq;

        then (p + q) <> ( 0_. R) by lemlp0;

        then

         D4: ( min* cpq) >= ( min* cp) by A, lemlowp1a2;

         not (( min* cpq) > ( min* cp)) by D1, NAT_1:def 1;

        hence thesis by A, D4, XXREAL_0: 1;

      end;

    end;

    theorem :: REALALG1:12

    

     lemlowp3a: for R be non degenerated Ring, p,q be non zero Polynomial of R st (p *' q) <> ( 0_. R) holds ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) }) >= (( min* { i where i be Nat : (p . i) <> ( 0. R) }) + ( min* { i where i be Nat : (q . i) <> ( 0. R) }))

    proof

      let R be non degenerated Ring, p,q be non zero Polynomial of R;

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      assume (p *' q) <> ( 0_. R);

      then (p *' q) is non zero;

      then

      reconsider cpq = { i where i be Nat : ((p *' q) . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      set m = (( min* cp) + ( min* cq));

      

       A: ( min* cpq) in cpq by NAT_1:def 1;

      now

        let z1 be Nat;

        assume z1 in cpq;

        then

        consider w be Nat such that

         H1: w = z1 & ((p *' q) . w) <> ( 0. R);

        reconsider z = z1 as Element of NAT by ORDINAL1:def 12;

        consider r1 be FinSequence of the carrier of R such that

         R: ( len r1) = (z + 1) & ((p *' q) . z) = ( Sum r1) & for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((p . (k -' 1)) * (q . ((z + 1) -' k))) by POLYNOM3:def 9;

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

        then

         A1: 1 in ( dom r1) by FINSEQ_3: 25, R;

        now

          assume

           AA1: z < m;

          

           F: for k be Nat st k in ( dom r1) holds (p . (k -' 1)) = ( 0. R) or (q . ((z + 1) -' k)) = ( 0. R)

          proof

            let k be Nat;

            assume k in ( dom r1);

            then

             EF: 1 <= k & k <= ( len r1) by FINSEQ_3: 25;

            per cases ;

              suppose

               AA0: (k -' 1) >= ( min* cp);

              

               AA2: (k -' 1) = (k - 1) by EF, XREAL_0:def 2;

              ((z + 1) - k) in NAT by INT_1: 5, R, EF;

              then ((z + 1) -' k) = ((z + 1) - k) by XREAL_0:def 2;

              then ((k -' 1) + ((z + 1) -' k)) < (( min* cp) + ( min* cq)) by AA1, AA2;

              then

               S: ((z + 1) -' k) < ( min* cq) by AA0, XREAL_1: 7;

              now

                assume (q . ((z + 1) -' k)) <> ( 0. R);

                then ((z + 1) -' k) in cq;

                hence contradiction by S, NAT_1:def 1;

              end;

              hence thesis;

            end;

              suppose

               S: (k -' 1) < ( min* cp);

              now

                assume (p . (k -' 1)) <> ( 0. R);

                then (k -' 1) in cp;

                hence contradiction by S, NAT_1:def 1;

              end;

              hence thesis;

            end;

          end;

          now

            let k be Element of NAT ;

            assume

             E: k in ( dom r1) & k <> 1;

            per cases by F, E;

              suppose (p . (k -' 1)) = ( 0. R);

              then (r1 . k) = (( 0. R) * (q . ((z + 1) -' k))) by E, R;

              hence (r1 /. k) = ( 0. R) by E, PARTFUN1:def 6;

            end;

              suppose (q . ((z + 1) -' k)) = ( 0. R);

              then (r1 . k) = ((p . (k -' 1)) * ( 0. R)) by E, R;

              hence (r1 /. k) = ( 0. R) by E, PARTFUN1:def 6;

            end;

          end;

          

          then

           T: ( Sum r1) = (r1 /. 1) by A1, POLYNOM2: 3

          .= (r1 . 1) by A1, PARTFUN1:def 6

          .= ((p . (1 -' 1)) * (q . ((z + 1) -' 1))) by A1, R;

          now

            per cases by A1, F;

              suppose (p . (1 -' 1)) = ( 0. R);

              hence ( Sum r1) = ( 0. R) by T;

            end;

              suppose (q . ((z + 1) -' 1)) = ( 0. R);

              hence ( Sum r1) = ( 0. R) by T;

            end;

          end;

          hence contradiction by H1, R;

        end;

        hence z1 >= m;

      end;

      hence thesis by A;

    end;

    theorem :: REALALG1:13

    

     lemlowp3b: for R be domRing, p,q be non zero Polynomial of R holds ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) }) = (( min* { i where i be Nat : (p . i) <> ( 0. R) }) + ( min* { i where i be Nat : (q . i) <> ( 0. R) }))

    proof

      let R be domRing, p,q be non zero Polynomial of R;

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) }, cpq = { i where i be Nat : ((p *' q) . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      set m = (( min* cp) + ( min* cq));

      consider r be FinSequence of the carrier of R such that

       M: ( len r) = (m + 1) & ((p *' q) . m) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((m + 1) -' k))) by POLYNOM3:def 9;

      

       B1: 1 <= (( min* cp) + 1) by NAT_1: 11;

      (( min* cp) + 1) <= ((( min* cp) + 1) + ( min* cq)) by NAT_1: 11;

      then (( min* cp) + 1) in ( Seg (m + 1)) by B1, FINSEQ_1: 1;

      then

       A1: (( min* cp) + 1) in ( dom r) by M, FINSEQ_1:def 3;

      

       A2: ((( min* cp) + 1) - 1) >= 0 ;

      

       A4: ((m + 1) -' (( min* cp) + 1)) = ((m + 1) - (( min* cp) + 1)) by XREAL_0:def 2;

      now

        let k be Element of NAT ;

        assume

         E: k in ( dom r) & k <> (( min* cp) + 1);

        then

         EE: 1 <= k <= (m + 1) by M, FINSEQ_3: 25;

        per cases by E, XXREAL_0: 1;

          suppose

           E1: k < (( min* cp) + 1);

          reconsider k1 = (k - 1) as Element of NAT by EE, INT_1: 3;

          

           E4: (k -' 1) = (k - 1) by EE, XREAL_0:def 2;

          then

           E3: (k -' 1) < ((( min* cp) + 1) - 1) by E1, XREAL_1: 9;

          now

            assume (p . k1) <> ( 0. R);

            then k1 in cp;

            hence contradiction by E3, E4, NAT_1:def 1;

          end;

          then (r . k) = (( 0. R) * (q . ((m + 1) -' k))) by E4, E, M;

          hence (r /. k) = ( 0. R) by E, PARTFUN1:def 6;

        end;

          suppose k > (( min* cp) + 1);

          then

           E1: ((m + 1) - k) < ((m + 1) - (( min* cp) + 1)) by XREAL_1: 10;

          ((m + 1) - k) in NAT by EE, INT_1: 5;

          then

           E3: ((m + 1) -' k) < ( min* cq) by E1, XREAL_0:def 2;

          now

            assume (q . ((m + 1) -' k)) <> ( 0. R);

            then ((m + 1) -' k) in cq;

            hence contradiction by E3, NAT_1:def 1;

          end;

          then (r . k) = ((p . (k -' 1)) * ( 0. R)) by E, M;

          hence (r /. k) = ( 0. R) by E, PARTFUN1:def 6;

        end;

      end;

      

      then

       X: ( Sum r) = (r /. (( min* cp) + 1)) by A1, POLYNOM2: 3

      .= (r . (( min* cp) + 1)) by A1, PARTFUN1:def 6

      .= ((p . ((( min* cp) + 1) -' 1)) * (q . ((m + 1) -' (( min* cp) + 1)))) by A1, M

      .= ((p . ( min* cp)) * (q . ( min* cq))) by A4, A2, XREAL_0:def 2;

      ( min* cp) in cp by NAT_1:def 1;

      then

      consider u be Nat such that

       H1: u = ( min* cp) & (p . u) <> ( 0. R);

      ( min* cq) in cq by NAT_1:def 1;

      then

      consider v be Nat such that

       H2: v = ( min* cq) & (q . v) <> ( 0. R);

      ((p . u) * (q . v)) <> ( 0. R) by H1, H2, VECTSP_2:def 1;

      then m in { i where i be Nat : ((p *' q) . i) <> ( 0. R) } by H1, H2, X, M;

      then

       C1: ( min* cpq) <= m by NAT_1:def 1;

      (p *' q) <> ( 0_. R);

      then ( min* cpq) >= m by lemlowp3a;

      hence thesis by C1, XXREAL_0: 1;

    end;

    begin

    definition

      let L be non empty multLoopStr;

      let S be Subset of L;

      :: REALALG1:def5

      attr S is mult-closed means for s1,s2 be Element of L st s1 in S & s2 in S holds (s1 * s2) in S;

    end

    definition

      let L be non empty addLoopStr;

      let S be Subset of L;

      :: REALALG1:def6

      func - S -> Subset of L equals { ( - s) where s be Element of L : s in S };

      coherence

      proof

        set M = { ( - s) where s be Element of L : s in S };

        now

          let x be object;

          assume x in M;

          then

          consider s be Element of L such that

           A1: x = ( - s) & s in S;

          thus x in the carrier of L by A1;

        end;

        then M c= the carrier of L;

        hence thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let S be Subset of L;

      reduce ( - ( - S)) to S;

      reducibility

      proof

         A:

        now

          let x be object;

          assume x in ( - ( - S));

          then

          consider a be Element of L such that

           A: x = ( - a) & a in ( - S);

          consider b be Element of L such that

           B: ( - b) = a & b in S by A;

          thus x in S by A, B;

        end;

        now

          let x be object;

          assume

           AS: x in S;

          then

          reconsider y = x as Element of L;

          consider a be Element of L such that

           A: ( - y) = ( - a) & a in S by AS;

          consider b be Element of L such that

           C: ( - b) = ( - a) & b in S by A;

          

           B: ( - a) in { ( - s) where s be Element of L : s in S } by A;

          y = ( - ( - b)) by A, C;

          hence x in ( - ( - S)) by C, B;

        end;

        hence thesis by A, TARSKI: 2;

      end;

    end

    theorem :: REALALG1:14

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for S be Subset of L holds for a be Element of L holds a in S iff ( - a) in ( - S)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let S be Subset of L, a be Element of L;

      now

        assume ( - a) in ( - S);

        then ( - ( - a)) in ( - ( - S));

        hence a in S;

      end;

      hence thesis;

    end;

    theorem :: REALALG1:15

    

     min1: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for S1,S2 be Subset of L holds ( - (S1 /\ S2)) = (( - S1) /\ ( - S2))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr, S1,S2 be Subset of L;

       A:

      now

        let o be object;

        assume o in ( - (S1 /\ S2));

        then

        consider s be Element of L such that

         A: ( - s) = o & s in (S1 /\ S2);

        s in S1 & s in S2 by A, XBOOLE_0:def 4;

        then ( - s) in ( - S1) & ( - s) in ( - S2);

        hence o in (( - S1) /\ ( - S2)) by A, XBOOLE_0:def 4;

      end;

      now

        let o be object;

        assume o in (( - S1) /\ ( - S2));

        then

         A: o in ( - S1) & o in ( - S2) by XBOOLE_0:def 4;

        then

        consider s1 be Element of L such that

         B: ( - s1) = o & s1 in S1;

        consider s2 be Element of L such that

         C: ( - s2) = o & s2 in S2 by A;

        s1 = ( - ( - s2)) by B, C

        .= s2;

        then s1 in (S1 /\ S2) by B, C, XBOOLE_0:def 4;

        hence o in ( - (S1 /\ S2)) by B;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: REALALG1:16

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for S1,S2 be Subset of L holds ( - (S1 \/ S2)) = (( - S1) \/ ( - S2))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr, S1,S2 be Subset of L;

       A:

      now

        let o be object;

        assume o in ( - (S1 \/ S2));

        then

        consider s be Element of L such that

         A: ( - s) = o & s in (S1 \/ S2);

        s in S1 or s in S2 by A, XBOOLE_0:def 3;

        then ( - s) in ( - S1) or ( - s) in ( - S2);

        hence o in (( - S1) \/ ( - S2)) by A, XBOOLE_0:def 3;

      end;

      now

        let o be object;

        assume

         A: o in (( - S1) \/ ( - S2));

        per cases by A, XBOOLE_0:def 3;

          suppose o in ( - S1);

          then

          consider s1 be Element of L such that

           B: ( - s1) = o & s1 in S1;

          s1 in (S1 \/ S2) by B, XBOOLE_0:def 3;

          hence o in ( - (S1 \/ S2)) by B;

        end;

          suppose o in ( - S2);

          then

          consider s1 be Element of L such that

           B: ( - s1) = o & s1 in S2;

          s1 in (S1 \/ S2) by B, XBOOLE_0:def 3;

          hence o in ( - (S1 \/ S2)) by B;

        end;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    definition

      let L be non empty addLoopStr;

      let S be Subset of L;

      :: REALALG1:def7

      attr S is negative-disjoint means

      : defneg: (S /\ ( - S)) = {( 0. L)};

    end

    definition

      let L be non empty addLoopStr;

      let S be Subset of L;

      :: REALALG1:def8

      attr S is spanning means

      : defsp: (S \/ ( - S)) = the carrier of L;

    end

    begin

    notation

      let R be Ring;

      let a be Element of R;

      synonym a is square for a is being_a_square;

    end

    registration

      let R be Ring;

      cluster ( 0. R) -> square;

      coherence

      proof

        ( 0. R) = (( 0. R) ^2 );

        hence thesis;

      end;

      cluster ( 1. R) -> square;

      coherence

      proof

        ( 1. R) = (( 1. R) ^2 );

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      cluster square for Element of R;

      existence

      proof

        take ( 1. R);

        thus thesis;

      end;

    end

    definition

      let R be Ring;

      let a be Element of R;

      :: REALALG1:def9

      attr a is sum_of_squares means ex f be FinSequence of R st ( Sum f) = a & for i be Nat st i in ( dom f) holds ex a be Element of R st (f . i) = (a ^2 );

    end

    

     AS0: for R be Ring holds for a be Element of R st a is square holds a is sum_of_squares

    proof

      let R be Ring, a be Element of R;

      assume

       AS: a is square;

      set f = <*a*>;

      

       A: ( Sum f) = a by RLVECT_1: 44;

      now

        let i be Nat;

        assume i in ( dom f);

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

        then i = 1 by TARSKI:def 1;

        hence ex b be Element of R st (f . i) = (b ^2 ) by AS, FINSEQ_1: 40;

      end;

      hence thesis by A;

    end;

    registration

      let R be Ring;

      cluster square -> sum_of_squares for Element of R;

      coherence by AS0;

    end

    

     S1: for R be Ring holds for a,b be Element of R st a is sum_of_squares & b is sum_of_squares holds (a + b) is sum_of_squares

    proof

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

      assume

       AS: a is sum_of_squares & b is sum_of_squares;

      then

      consider f be FinSequence of R such that

       A: ( Sum f) = a & for i be Nat st i in ( dom f) holds ex a be Element of R st (f . i) = (a ^2 );

      consider g be FinSequence of R such that

       B: ( Sum g) = b & for i be Nat st i in ( dom g) holds ex a be Element of R st (g . i) = (a ^2 ) by AS;

      set t = (f ^ g);

      

       C: ( Sum t) = (a + b) by A, B, RLVECT_1: 41;

      now

        let i be Nat;

        assume

         D: i in ( dom t);

        per cases by D, FINSEQ_1: 25;

          suppose

           E: i in ( dom f);

          then (t . i) = (f . i) by FINSEQ_1:def 7;

          hence ex x be Element of R st (t . i) = (x ^2 ) by E, A;

        end;

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

          then

          consider n be Nat such that

           E: n in ( dom g) & i = (( len f) + n);

          (t . i) = (g . n) by E, FINSEQ_1:def 7;

          hence ex x be Element of R st (t . i) = (x ^2 ) by E, B;

        end;

      end;

      hence thesis by C;

    end;

    

     S2: for R be commutative Ring holds for a,b be Element of R st a is square & b is sum_of_squares holds (a * b) is sum_of_squares

    proof

      let R be commutative Ring, a,b be Element of R;

      assume

       AS: a is square & b is sum_of_squares;

      then

      consider f be FinSequence of R such that

       A: ( Sum f) = b & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 );

      set g = (a * f);

      

       B: ( Sum g) = (a * b) by A, BINOM: 4;

      now

        let i be Nat;

        assume

         C: i in ( dom g);

        then

         D: i in ( dom f) by POLYNOM1:def 1;

        

         E: (g . i) = (g /. i) by C, PARTFUN1:def 6

        .= (a * (f /. i)) by D, POLYNOM1:def 1;

        consider x be Element of R such that

         F: (f . i) = (x ^2 ) by D, A;

        consider y be Element of R such that

         G: a = (y ^2 ) by AS;

        (g . i) = ((y ^2 ) * (x ^2 )) by E, G, D, F, PARTFUN1:def 6

        .= (x * (x * (y * y))) by GROUP_1:def 3

        .= (x * ((x * y) * y)) by GROUP_1:def 3

        .= ((x * y) ^2 ) by GROUP_1:def 3;

        hence ex z be Element of R st (g . i) = (z ^2 );

      end;

      hence thesis by B;

    end;

    

     SM1: for R be commutative Ring holds for a,b be Element of R st a is square & b is square holds (a * b) is square

    proof

      let R be commutative Ring, a,b be Element of R;

      assume

       AS: a is square & b is square;

      then

      consider x be Element of R such that

       A: a = (x ^2 );

      consider y be Element of R such that

       B: b = (y ^2 ) by AS;

      (a * b) = (x * (x * (y * y))) by GROUP_1:def 3, A, B

      .= (x * (y * (x * y))) by GROUP_1:def 3

      .= ((x * y) ^2 ) by GROUP_1:def 3;

      hence thesis;

    end;

    

     S3: for R be commutative Ring holds for a,b be Element of R st a is sum_of_squares & b is sum_of_squares holds (a * b) is sum_of_squares

    proof

      let R be commutative Ring, a,b be Element of R;

      assume

       AS: a is sum_of_squares & b is sum_of_squares;

      defpred P[ Nat] means for f be FinSequence of R st ( len f) = $1 & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 ) holds (a * ( Sum f)) is sum_of_squares;

      now

        let f be FinSequence of R;

        assume ( len f) = 0 & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 );

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

        then ( Sum f) = ( 0. R) by RLVECT_1: 43;

        hence (a * ( Sum f)) is sum_of_squares;

      end;

      then

       A: P[ 0 ];

       B:

      now

        let k be Nat;

        assume

         IV: P[k];

        now

          let f be FinSequence of R;

          assume

           B0: ( len f) = (k + 1) & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 );

          then f <> {} ;

          then

          consider g be FinSequence, x be object such that

           B1: f = (g ^ <*x*>) by FINSEQ_1: 46;

          reconsider g, h = <*x*> as FinSequence of R by B1, FINSEQ_1: 36;

          ( len h) = 1 by FINSEQ_1: 39;

          then

           B2: ( len f) = (( len g) + 1) by B1, FINSEQ_1: 22;

          now

            let i be Nat;

            assume

             C1: i in ( dom g);

            then

             C2: (g . i) = (f . i) by B1, FINSEQ_1:def 7;

            ( dom g) c= ( dom f) by B1, FINSEQ_1: 26;

            hence ex x be Element of R st (g . i) = (x ^2 ) by B0, C2, C1;

          end;

          then

           B3: (a * ( Sum g)) is sum_of_squares by IV, B2, B0;

          

           C2: ( dom f) = ( Seg (k + 1)) by B0, FINSEQ_1:def 3;

          

           B4: 1 <= (k + 1) by NAT_1: 11;

          

           B5: x = (f . (k + 1)) by B0, B2, B1, FINSEQ_1: 42;

          then

          reconsider x as Element of R by B4, C2, FINSEQ_1: 1, FINSEQ_2: 11;

          consider z be Element of R such that

           B6: x = (z ^2 ) by B0, B4, B5, C2, FINSEQ_1: 1;

          x is square by B6;

          then

           B7: (x * a) is sum_of_squares by S2, AS;

          ((a * ( Sum g)) + (a * x)) = (a * (( Sum g) + x)) by VECTSP_1:def 3

          .= (a * (( Sum g) + ( Sum <*x*>))) by RLVECT_1: 44

          .= (a * ( Sum f)) by B1, RLVECT_1: 41;

          hence (a * ( Sum f)) is sum_of_squares by B7, B3, S1;

        end;

        hence P[(k + 1)];

      end;

      

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

      consider f be FinSequence of R such that

       H: ( Sum f) = b & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 ) by AS;

      consider k be Nat such that

       K: ( len f) = k;

      thus thesis by I, H, K;

    end;

    registration

      let R be commutative Ring;

      let a,b be square Element of R;

      cluster (a * b) -> square;

      coherence by SM1;

    end

    registration

      let R be Ring;

      let a,b be sum_of_squares Element of R;

      cluster (a + b) -> sum_of_squares;

      coherence by S1;

    end

    registration

      let R be commutative Ring;

      let a,b be sum_of_squares Element of R;

      cluster (a * b) -> sum_of_squares;

      coherence by S3;

    end

    definition

      let R be Ring;

      :: REALALG1:def10

      func Squares_of R -> Subset of R equals { a where a be Element of R : a is square };

      coherence

      proof

        set M = { a where a be Element of R : a is square };

        now

          let x be object;

          assume x in M;

          then

          consider a be Element of R such that

           A1: x = a & a is square;

          thus x in the carrier of R by A1;

        end;

        then M c= the carrier of R;

        hence thesis;

      end;

      :: REALALG1:def11

      func Quadratic_Sums_of R -> Subset of R equals { a where a be Element of R : a is sum_of_squares };

      coherence

      proof

        set M = { a where a be Element of R : a is sum_of_squares };

        now

          let x be object;

          assume x in M;

          then

          consider a be Element of R such that

           A1: x = a & a is sum_of_squares;

          thus x in the carrier of R by A1;

        end;

        then M c= the carrier of R;

        hence thesis;

      end;

    end

    notation

      let R be Ring;

      synonym SQ R for Squares_of R;

      synonym QS R for Quadratic_Sums_of R;

    end

    

     SQ0: for R be Ring holds ( 0. R) in ( SQ R);

    

     QS0: for R be Ring holds ( 0. R) in ( QS R);

    registration

      let R be Ring;

      cluster ( SQ R) -> non empty;

      coherence by SQ0;

      cluster ( QS R) -> non empty;

      coherence by QS0;

    end

    definition

      let R be Ring;

      let S be Subset of R;

      :: REALALG1:def12

      attr S is with_squares means ( SQ R) c= S;

      :: REALALG1:def13

      attr S is with_sums_of_squares means ( QS R) c= S;

    end

    registration

      let R be Ring;

      cluster with_squares for Subset of R;

      existence

      proof

        take ( SQ R);

        thus thesis;

      end;

      cluster with_sums_of_squares for Subset of R;

      existence

      proof

        take ( QS R);

        thus thesis;

      end;

    end

    registration

      let R be Ring;

      cluster with_squares -> non empty for Subset of R;

      coherence ;

      cluster with_sums_of_squares -> non empty for Subset of R;

      coherence ;

    end

    registration

      let R be Ring;

      cluster with_sums_of_squares -> with_squares for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         AS: S is with_sums_of_squares;

        ( SQ R) c= S

        proof

          let o be object;

          assume o in ( SQ R);

          then

          consider a be Element of R such that

           A: o = a & a is square;

          a in ( QS R) by A;

          hence o in S by A, AS;

        end;

        hence thesis;

      end;

      cluster with_squares add-closed -> with_sums_of_squares for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         AS: S is with_squares add-closed;

        defpred P[ Nat] means for f be FinSequence of R st ( len f) = $1 & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 ) holds ( Sum f) in S;

        now

          let f be FinSequence of R;

          assume ( len f) = 0 & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 );

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

          then ( Sum f) = ( 0. R) by RLVECT_1: 43;

          then ( Sum f) in ( SQ R);

          hence ( Sum f) in S by AS;

        end;

        then

         A: P[ 0 ];

         B:

        now

          let k be Nat;

          assume

           IV: P[k];

          now

            let f be FinSequence of R;

            assume

             B0: ( len f) = (k + 1) & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 );

            then f <> {} ;

            then

            consider g be FinSequence, x be object such that

             B1: f = (g ^ <*x*>) by FINSEQ_1: 46;

            reconsider g, h = <*x*> as FinSequence of R by B1, FINSEQ_1: 36;

            ( len h) = 1 by FINSEQ_1: 39;

            then

             B2: ( len f) = (( len g) + 1) by B1, FINSEQ_1: 22;

            now

              let i be Nat;

              assume

               C1: i in ( dom g);

              then

               C2: (g . i) = (f . i) by B1, FINSEQ_1:def 7;

              ( dom g) c= ( dom f) by B1, FINSEQ_1: 26;

              hence ex x be Element of R st (g . i) = (x ^2 ) by B0, C2, C1;

            end;

            then

             B3: ( Sum g) in S by IV, B2, B0;

            

             C2: ( dom f) = ( Seg (k + 1)) by B0, FINSEQ_1:def 3;

            

             B4: 1 <= (k + 1) by NAT_1: 11;

            

             B5: x = (f . (k + 1)) by B0, B2, B1, FINSEQ_1: 42;

            then

            reconsider x as Element of R by B4, C2, FINSEQ_1: 1, FINSEQ_2: 11;

            consider z be Element of R such that

             B6: x = (z ^2 ) by B0, B4, B5, C2, FINSEQ_1: 1;

            x is square by B6;

            then

             B7: x in ( SQ R);

            (( Sum g) + x) = (( Sum g) + ( Sum <*x*>)) by RLVECT_1: 44

            .= ( Sum f) by B1, RLVECT_1: 41;

            hence ( Sum f) in S by B7, B3, AS;

          end;

          hence P[(k + 1)];

        end;

        

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

        now

          let o be object;

          assume o in ( QS R);

          then

          consider a be Element of R such that

           A: o = a & a is sum_of_squares;

          consider f be FinSequence of R such that

           B: ( Sum f) = o & for i be Nat st i in ( dom f) holds ex x be Element of R st (f . i) = (x ^2 ) by A;

          consider n be Nat such that

           H: ( len f) = n;

          thus o in S by H, B, I;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let R be Ring;

      cluster ( SQ R) -> with_squares;

      coherence ;

      cluster ( QS R) -> with_sums_of_squares;

      coherence ;

    end

    theorem :: REALALG1:17

    for R be Ring holds ( 0. R) in ( SQ R) & ( 1. R) in ( SQ R);

    theorem :: REALALG1:18

    for R be Ring holds ( SQ R) c= ( QS R)

    proof

      let R be Ring;

      let o be object;

      assume o in ( SQ R);

      then

      consider a be Element of R such that

       A: o = a & a is square;

      thus o in ( QS R) by A;

    end;

    registration

      let R be Ring;

      cluster ( QS R) -> add-closed;

      coherence

      proof

        let x,y be Element of R;

        assume

         AS: x in ( QS R) & y in ( QS R);

        then

        consider a be Element of R such that

         A: x = a & a is sum_of_squares;

        consider b be Element of R such that

         B: y = b & b is sum_of_squares by AS;

        thus (x + y) in ( QS R) by A, B;

      end;

    end

    registration

      let R be commutative Ring;

      cluster ( QS R) -> mult-closed;

      coherence

      proof

        let x,y be Element of R;

        assume

         AS: x in ( QS R) & y in ( QS R);

        then

        consider a be Element of R such that

         A: x = a & a is sum_of_squares;

        consider b be Element of R such that

         B: y = b & b is sum_of_squares by AS;

        thus (x * y) in ( QS R) by A, B;

      end;

    end

    

     lemminus: for R be Ring, S be Subring of R, a be Element of R, b be Element of S st a = b holds ( - a) = ( - b)

    proof

      let R be Ring, S be Subring of R, a be Element of R, b be Element of S;

      assume

       AS: a = b;

      the carrier of S c= the carrier of R by C0SP1:def 3;

      then

      reconsider c = ( - b) as Element of R;

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

      then

       A6: [c, a] in ( dom the addF of S) by AS, ZFMISC_1:def 2;

      (c + a) = ((the addF of R || the carrier of S) . (c,a)) by A6, FUNCT_1: 49

      .= (( - b) + b) by AS, C0SP1:def 3

      .= ( 0. S) by RLVECT_1: 5

      .= ( 0. R) by C0SP1:def 3

      .= (( - a) + a) by RLVECT_1: 5;

      hence thesis by RLVECT_1: 8;

    end;

    

     lemminus1: for R be Ring, S be Subring of R, S1 be Subset of R, S2 be Subset of S st S1 = S2 holds ( - S1) = ( - S2)

    proof

      let R be Ring, S be Subring of R, S1 be Subset of R, S2 be Subset of S;

      assume

       AS: S1 = S2;

      hereby

        let o be object;

        assume o in ( - S1);

        then

        consider a be Element of R such that

         A1: ( - a) = o & a in S1;

        reconsider b = a as Element of S by A1, AS;

        ( - b) in ( - S2) by A1, AS;

        hence o in ( - S2) by A1, lemminus;

      end;

      let o be object;

      assume o in ( - S2);

      then

      consider a be Element of S such that

       A1: ( - a) = o & a in S2;

      reconsider b = a as Element of R by A1, AS;

      ( - b) in ( - S1) by A1, AS;

      hence o in ( - S1) by A1, lemminus;

    end;

    

     lemsum: for R be Ring, S be Subring of R, f be FinSequence of R, g be FinSequence of S st f = g holds ( Sum f) = ( Sum g)

    proof

      let R be Ring, S be Subring of R, f be FinSequence of R, g be FinSequence of S;

      assume

       AS: f = g;

      defpred P[ Nat] means for f be FinSequence of R, g be FinSequence of S st f = g & ( len f) = $1 holds ( Sum f) = ( Sum g);

      now

        let f be FinSequence of R, g be FinSequence of S;

        assume f = g & ( len f) = 0 ;

        then

         A: f = ( <*> the carrier of R) & g = ( <*> the carrier of S);

        

        hence ( Sum f) = ( 0. R) by RLVECT_1: 43

        .= ( 0. S) by C0SP1:def 3

        .= ( Sum g) by A, RLVECT_1: 43;

      end;

      then

       A: P[ 0 ];

      

       AS4: the carrier of S c= the carrier of R by C0SP1:def 3;

       B:

      now

        let k be Nat;

        assume

         IA: P[k];

        now

          let f be FinSequence of R, g be FinSequence of S;

          assume

           B0: f = g & ( len f) = (k + 1);

          then g <> {} ;

          then

          consider h be FinSequence, x be object such that

           B1: g = (h ^ <*x*>) by FINSEQ_1: 46;

          reconsider h, o = <*x*> as FinSequence of S by B1, FINSEQ_1: 36;

          ( len o) = 1 by FINSEQ_1: 39;

          then

           B2: ( len g) = (( len h) + 1) by B1, FINSEQ_1: 22;

          

           C2: ( dom g) = ( Seg (k + 1)) by B0, FINSEQ_1:def 3;

          

           B4: 1 <= (k + 1) by NAT_1: 11;

          x = (g . (k + 1)) by B0, B2, B1, FINSEQ_1: 42;

          then

          reconsider x as Element of S by B4, C2, FINSEQ_1: 1, FINSEQ_2: 11;

          reconsider y = x as Element of R by AS4;

          ( rng h) c= the carrier of R by AS4;

          then

          reconsider hh = h as FinSequence of R by FINSEQ_1:def 4;

          ( rng o) c= the carrier of R by AS4;

          then

          reconsider oo = o as FinSequence of R by FINSEQ_1:def 4;

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

          then

           B7: [( Sum h), ( Sum o)] in ( dom the addF of S);

          

           B8: ( Sum o) = y by RLVECT_1: 44

          .= ( Sum oo) by RLVECT_1: 44;

          

          thus ( Sum f) = (( Sum hh) + ( Sum oo)) by B0, B1, RLVECT_1: 41

          .= (the addF of R . (( Sum h),( Sum o))) by B8, B0, B2, IA

          .= ((the addF of R || the carrier of S) . (( Sum h),( Sum o))) by B7, FUNCT_1: 49

          .= (( Sum h) + ( Sum o)) by C0SP1:def 3

          .= ( Sum g) by B1, RLVECT_1: 41;

        end;

        hence P[(k + 1)];

      end;

      

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

      consider n be Nat such that

       H: ( len f) = n;

      thus thesis by AS, I, H;

    end;

    theorem :: REALALG1:19

    

     SQsub: for R be Ring holds for S be Subring of R holds ( SQ S) c= ( SQ R)

    proof

      let R be Ring, S be Subring of R;

      

       AS4: the carrier of S c= the carrier of R by C0SP1:def 3;

      let o be object;

      assume o in ( SQ S);

      then

      consider a be Element of S such that

       A: o = a & a is square;

      consider b be Element of S such that

       B: a = (b ^2 ) by A;

      reconsider a1 = a, b1 = b as Element of R by AS4;

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

      then

       B6: [b, b] in ( dom the multF of S);

      a1 = ((the multF of R || the carrier of S) . (b,b)) by C0SP1:def 3, B

      .= (b1 ^2 ) by B6, FUNCT_1: 49;

      then a1 is square;

      hence o in ( SQ R) by A;

    end;

    theorem :: REALALG1:20

    for R be Ring holds for S be Subring of R holds ( QS S) c= ( QS R)

    proof

      let R be Ring, S be Subring of R;

      

       AS4: the carrier of S c= the carrier of R by C0SP1:def 3;

      let o be object;

      assume o in ( QS S);

      then

      consider a be Element of S such that

       D2: a = o & a is sum_of_squares;

      consider f be FinSequence of S such that

       D3: ( Sum f) = a & for i be Nat st i in ( dom f) holds ex a be Element of S st (f . i) = (a ^2 ) by D2;

      reconsider a1 = a as Element of R by AS4;

      ( rng f) c= the carrier of R by AS4;

      then

      reconsider g = f as FinSequence of R by FINSEQ_1:def 4;

      

       D9: ( Sum g) = ( Sum f) by lemsum;

      now

        let i be Nat;

        assume i in ( dom g);

        then

        consider a be Element of S such that

         E1: (f . i) = (a ^2 ) by D3;

        reconsider a1 = a as Element of R by AS4;

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

        then

         B6: [a, a] in ( dom the multF of S);

        (a1 ^2 ) = ((the multF of R || the carrier of S) . (a,a)) by B6, FUNCT_1: 49

        .= (a ^2 ) by C0SP1:def 3;

        hence ex a be Element of R st (g . i) = (a ^2 ) by E1;

      end;

      then a1 is sum_of_squares by D3, D9;

      hence o in ( QS R) by D2;

    end;

    begin

    definition

      let R be Ring, S be Subset of R;

      :: REALALG1:def14

      attr S is prepositive_cone means

      : defppc: (S + S) c= S & (S * S) c= S & (S /\ ( - S)) = {( 0. R)} & ( SQ R) c= S;

      :: REALALG1:def15

      attr S is positive_cone means

      : defpc: (S + S) c= S & (S * S) c= S & (S /\ ( - S)) = {( 0. R)} & (S \/ ( - S)) = the carrier of R;

    end

    registration

      let R be Ring;

      cluster prepositive_cone -> non empty for Subset of R;

      coherence ;

      cluster positive_cone -> non empty for Subset of R;

      coherence ;

    end

    registration

      let R be Ring;

      cluster prepositive_cone -> add-closed mult-closed negative-disjoint with_squares for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         AS: S is prepositive_cone;

        thus S is add-closed

        proof

          let x,y be Element of R;

          assume x in S & y in S;

          then (x + y) in { (a + b) where a,b be Element of R : a in S & b in S };

          then (x + y) in (S + S) by IDEAL_1:def 19;

          hence (x + y) in S by AS;

        end;

        thus S is mult-closed

        proof

          let x,y be Element of R;

          assume x in S & y in S;

          then (x * y) in (S * S);

          hence (x * y) in S by AS;

        end;

        thus S is negative-disjoint with_squares by AS;

      end;

      cluster add-closed mult-closed negative-disjoint with_squares -> prepositive_cone for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         AS: S is add-closed mult-closed negative-disjoint with_squares;

        

         B: (S + S) c= S

        proof

          let x be object;

          assume x in (S + S);

          then x in { (a + b) where a,b be Element of R : a in S & b in S } by IDEAL_1:def 19;

          then

          consider a,b be Element of R such that

           A1: x = (a + b) & a in S & b in S;

          thus x in S by AS, A1;

        end;

        (S * S) c= S

        proof

          let x be object;

          assume x in (S * S);

          then

          consider a,b be Element of R such that

           A1: x = (a * b) & a in S & b in S;

          thus x in S by A1, AS;

        end;

        hence thesis by AS, B;

      end;

    end

    registration

      let R be Ring;

      cluster positive_cone -> add-closed mult-closed negative-disjoint spanning for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         AS: S is positive_cone;

        thus S is add-closed

        proof

          let x,y be Element of R;

          assume x in S & y in S;

          then (x + y) in { (a + b) where a,b be Element of R : a in S & b in S };

          then (x + y) in (S + S) by IDEAL_1:def 19;

          hence (x + y) in S by AS;

        end;

        thus S is mult-closed

        proof

          let x,y be Element of R;

          assume x in S & y in S;

          then (x * y) in (S * S);

          hence (x * y) in S by AS;

        end;

        thus S is negative-disjoint spanning by AS;

      end;

      cluster add-closed mult-closed negative-disjoint spanning -> positive_cone for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         AS: S is add-closed mult-closed negative-disjoint spanning;

        

         B: (S + S) c= S

        proof

          let x be object;

          assume x in (S + S);

          then x in { (a + b) where a,b be Element of R : a in S & b in S } by IDEAL_1:def 19;

          then

          consider a,b be Element of R such that

           A1: x = (a + b) & a in S & b in S;

          thus x in S by AS, A1;

        end;

        (S * S) c= S

        proof

          let x be object;

          assume x in (S * S);

          then

          consider a,b be Element of R such that

           A1: x = (a * b) & a in S & b in S;

          thus x in S by A1, AS;

        end;

        hence thesis by AS, B;

      end;

    end

    registration

      let R be Ring;

      cluster positive_cone -> prepositive_cone for Subset of R;

      coherence

      proof

        let P be Subset of R;

        assume

         AS: P is positive_cone;

        ( SQ R) c= P

        proof

          let o be object;

          assume o in ( SQ R);

          then

          consider a be Element of R such that

           A: o = a & a is square;

          consider b be Element of R such that

           B: a = (b ^2 ) by A;

          per cases by AS, XBOOLE_0:def 3;

            suppose b in P;

            then (b * b) in { (x * y) where x,y be Element of R : x in P & y in P };

            hence o in P by A, B, AS;

          end;

            suppose b in ( - P);

            then

            consider b1 be Element of R such that

             D: ( - b1) = b & b1 in P;

            

             E: (b1 * b1) in { (x * y) where x,y be Element of R : x in P & y in P } by D;

            (b1 * b1) = (b * b) by D, VECTSP_1: 10;

            hence o in P by E, B, A, AS;

          end;

        end;

        hence thesis by AS;

      end;

    end

    theorem :: REALALG1:21

    

     X1: for F be Field holds for S be Subset of F st (S * S) c= S & ( SQ F) c= S holds (S /\ ( - S)) = {( 0. F)} iff not ( - ( 1. F)) in S

    proof

      let R be Field, S be Subset of R;

      assume

       AS: (S * S) c= S & ( SQ R) c= S;

      

       A0: ( 1. R) in ( SQ R);

       X:

      now

        assume

         A: (S /\ ( - S)) = {( 0. R)};

        now

          assume ( - ( 1. R)) in S;

          then ( - ( - ( 1. R))) in ( - S);

          then ( 1. R) in (S /\ ( - S)) by XBOOLE_0:def 4, A0, AS;

          hence contradiction by A, TARSKI:def 1;

        end;

        hence not ( - ( 1. R)) in S;

      end;

      now

        assume

         A: not ( - ( 1. R)) in S;

        now

          assume

           A2: (S /\ ( - S)) <> {( 0. R)};

          

           B0: ( 0. R) in ( SQ R);

          then ( - ( 0. R)) in ( - S) by AS;

          then ( 0. R) in (S /\ ( - S)) by AS, B0, XBOOLE_0:def 4;

          then

           A3: {( 0. R)} c= (S /\ ( - S)) by TARSKI:def 1;

          now

            assume

             A4: not (ex a be Element of R st a <> ( 0. R) & a in (S /\ ( - S)));

            now

              let o be object;

              assume o in (S /\ ( - S));

              then o = ( 0. R) by A4;

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

            end;

            hence contradiction by A2, A3, TARSKI: 2;

          end;

          then

          consider a be Element of R such that

           A5: a <> ( 0. R) & a in (S /\ ( - S));

          

           A9: a in S & a in ( - S) by A5, XBOOLE_0:def 4;

          then

           A6: ( - a) in ( - ( - S));

           A7:

          now

            assume ( - a) = ( 0. R);

            then ( - ( - a)) = ( 0. R);

            hence contradiction by A5;

          end;

          ((( - a) " ) ^2 ) is square;

          then ((( - a) " ) ^2 ) in ( SQ R);

          then

           A8: (((( - a) " ) ^2 ) * ( - a)) in (S * S) by AS, A6;

          (( - a) " ) in S

          proof

            (((( - a) " ) ^2 ) * ( - a)) = ((( - a) " ) * ((( - a) " ) * ( - a))) by GROUP_1:def 3

            .= ((( - a) " ) * ( 1. R)) by A7, VECTSP_1:def 10

            .= (( - a) " );

            hence thesis by A8, AS;

          end;

          then

           A8: (a * (( - a) " )) in (S * S) by A9;

          (( - (a " )) * ( - a)) = (a * (a " )) by VECTSP_1: 10

          .= ( 1. R) by A5, VECTSP_1:def 10;

          

          then (a * (( - a) " )) = (a * ( - (a " ))) by A7, VECTSP_1:def 10

          .= ( - (a * (a " ))) by VECTSP_1: 8

          .= ( - ( 1. R)) by A5, VECTSP_1:def 10;

          hence contradiction by A8, A, AS;

        end;

        hence (S /\ ( - S)) = {( 0. R)};

      end;

      hence thesis by X;

    end;

    theorem :: REALALG1:22

    for F be Field holds for S be Subset of F st (S * S) c= S & (S \/ ( - S)) = the carrier of F holds (S /\ ( - S)) = {( 0. F)} iff not ( - ( 1. F)) in S

    proof

      let F be Field, S be Subset of F;

      assume

       AS: (S * S) c= S & (S \/ ( - S)) = the carrier of F;

      ( SQ F) c= S

      proof

        let o be object;

        assume o in ( SQ F);

        then

        consider a be Element of F such that

         A: a = o & a is square;

        consider b be Element of F such that

         B: (b ^2 ) = a by A;

        per cases by AS, XBOOLE_0:def 3;

          suppose b in S;

          then (b * b) in (S * S);

          hence o in S by AS, A, B;

        end;

          suppose b in ( - S);

          then ( - b) in ( - ( - S));

          then (( - b) * ( - b)) in (S * S);

          then (( - b) * ( - b)) in S by AS;

          hence o in S by A, B, VECTSP_1: 10;

        end;

      end;

      hence thesis by X1, AS;

    end;

    definition

      let R be Ring;

      :: REALALG1:def16

      attr R is preordered means

      : defpord: ex P be Subset of R st P is prepositive_cone;

      :: REALALG1:def17

      attr R is ordered means

      : deford: ex P be Subset of R st P is positive_cone;

    end

    

     lemEX: for S be Subset of F_Real st S = { x where x be Element of REAL : 0 <= x } holds S is positive_cone

    proof

      let S be Subset of F_Real ;

      assume

       AS: S = { x where x be Element of REAL : 0 <= x };

      set R = F_Real ;

      

       A: (S + S) c= S

      proof

        let o be object;

        assume o in (S + S);

        then o in { (a + b) where a,b be Element of R : a in S & b in S } by IDEAL_1:def 19;

        then

        consider a,b be Element of R such that

         A: o = (a + b) & a in S & b in S;

        consider x be Element of R such that

         B: x = a & 0 <= x by A, AS;

        consider y be Element of R such that

         C: y = b & 0 <= y by A, AS;

        thus o in S by A, B, C, AS;

      end;

      

       B: (S * S) c= S

      proof

        let o be object;

        assume o in (S * S);

        then

        consider a,b be Element of R such that

         A: o = (a * b) & a in S & b in S;

        consider x be Element of R such that

         B: x = a & 0 <= x by A, AS;

        consider y be Element of R such that

         C: y = b & 0 <= y by A, AS;

        thus o in S by A, B, C, AS;

      end;

       K:

      now

        let o be object;

        assume

         K0: o in (S /\ ( - S));

        then

         K1: o in S & o in ( - S) by XBOOLE_0:def 4;

        reconsider x = o as Element of F_Real by K0;

        consider y1 be Element of R such that

         K2: y1 = o & 0 <= y1 by AS, K1;

        consider y2 be Element of R such that

         K3: ( - y2) = o & y2 in S by K1;

        consider y be Element of R such that

         K4: y2 = y & 0 <= y by AS, K3;

        y1 = ( 0. R) by K4, K2, K3;

        hence o in {( 0. R)} by K2, TARSKI:def 1;

      end;

       C:

      now

        let o be object;

        assume

         K0: o in {( 0. R)};

        then

         K1: o = ( 0. R) by TARSKI:def 1;

        reconsider x = o as Element of F_Real by K0;

        

         K2: 0 <= x & 0 <= ( - x) by K1;

        

         K3: x in S by AS, K0;

        x in { ( - s) where s be Element of R : s in S } by K2, K3, K1;

        hence o in (S /\ ( - S)) by K3, XBOOLE_0:def 4;

      end;

       F:

      now

        let o be object;

        assume o in the carrier of R;

        then

        reconsider x = o as Element of F_Real ;

        per cases ;

          suppose 0 <= x;

          then x in S by AS;

          hence o in (S \/ ( - S)) by XBOOLE_0:def 3;

        end;

          suppose 0 <= ( - x);

          then ( - x) in S by AS;

          then ( - ( - x)) in ( - S);

          hence o in (S \/ ( - S)) by XBOOLE_0:def 3;

        end;

      end;

      for o be object st o in (S \/ ( - S)) holds o in the carrier of R;

      hence S is positive_cone by A, B, C, K, F, TARSKI: 2;

    end;

    

     EX: F_Real is ordered

    proof

      set R = F_Real , S = { x where x be Element of REAL : 0 <= x };

      now

        let o be object;

        assume o in S;

        then

        consider x be Element of REAL such that

         A: o = x & 0 <= x;

        thus o in the carrier of F_Real by A;

      end;

      then

      reconsider S as Subset of F_Real by TARSKI:def 3;

      S is positive_cone by lemEX;

      hence thesis;

    end;

    registration

      cluster preordered for Field;

      existence

      proof

        take F_Real ;

        thus thesis by EX;

      end;

      cluster ordered for Field;

      existence by EX;

    end

    registration

      cluster ordered -> preordered for Ring;

      coherence ;

    end

    registration

      let R be preordered Ring;

      cluster prepositive_cone for Subset of R;

      existence by defpord;

    end

    registration

      let R be ordered Ring;

      cluster positive_cone for Subset of R;

      existence by deford;

    end

    definition

      let R be preordered Ring;

      mode Preordering of R is prepositive_cone Subset of R;

    end

    definition

      let R be ordered Ring;

      mode Ordering of R is positive_cone Subset of R;

    end

    theorem :: REALALG1:23

    

     ord1: for R be preordered Ring holds for P be Preordering of R holds for a be Element of R holds (a ^2 ) in P

    proof

      let R be preordered Ring, P be Preordering of R, a be Element of R;

      (a ^2 ) is square;

      then

       A: (a ^2 ) in ( SQ R);

      ( SQ R) c= P by defppc;

      hence thesis by A;

    end;

    theorem :: REALALG1:24

    

     ord2: for R be preordered Ring holds for P be Preordering of R holds ( QS R) c= P

    proof

      let R be preordered Ring, P be Preordering of R;

      P is with_sums_of_squares;

      hence thesis;

    end;

    theorem :: REALALG1:25

    

     ord3: for R be preordered Ring holds for P be Preordering of R holds ( 0. R) in P & ( 1. R) in P

    proof

      let R be preordered Ring, O be Preordering of R;

      ( 0. R) in ( QS R) & ( 1. R) in ( QS R);

      hence thesis by ord2, TARSKI:def 3;

    end;

    theorem :: REALALG1:26

    

     ord4: for R be preordered non degenerated Ring holds for P be Preordering of R holds not ( - ( 1. R)) in P

    proof

      let R be preordered non degenerated Ring, P be Preordering of R;

      

       A: ( 1. R) in P by ord3;

      assume ( - ( 1. R)) in P;

      then ( - ( - ( 1. R))) in ( - P);

      then ( 1. R) in (P /\ ( - P)) by XBOOLE_0:def 4, A;

      then ( 1. R) in {( 0. R)} by defppc;

      hence contradiction by TARSKI:def 1;

    end;

    theorem :: REALALG1:27

    

     ord5: for F be preordered Field holds for P be Preordering of F holds for a be non zero Element of F st a in P holds (a " ) in P

    proof

      let F be preordered Field;

      let P be Preordering of F;

      let a be non zero Element of F;

      assume

       A: a in P;

      

       E: a <> ( 0. F);

      set b = (a " );

      

       C: (P * P) c= P by defppc;

      (b * b) = (b ^2 );

      then (b * b) in P by ord1;

      then

       B: (a * (b * b)) in { (x * y) where x,y be Element of F : x in P & y in P } by A;

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

      .= (( 1. F) * b) by E, VECTSP_1:def 10

      .= b;

      hence thesis by B, C;

    end;

    theorem :: REALALG1:28

    

     tchar: for R be preordered non degenerated Ring holds ( Char R) = 0

    proof

      let R be preordered non degenerated Ring;

      set P = the Preordering of R;

      

       A: ( 1. R) in P by ord3;

      

       B: ( QS R) c= P by ord2;

      set n = ( Char R);

      now

        assume

         AS: ( Char R) <> 0 ;

        then

         C: (n '*' ( 1. R)) = ( 0. R) by RING_3:def 5;

        ((n '*' ( 1. R)) - ( 1. R)) = ((n '*' ( 1. R)) - (1 '*' ( 1. R))) by RING_3: 60;

        then

         F: ((n - 1) '*' ( 1. R)) = ( - ( 1. R)) by C, RING_3: 64;

        reconsider n1 = (n - 1) as Element of NAT by AS, INT_1: 3;

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

        consider f be FinSequence such that

         D: ( len f) = n1 & for k be Nat st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

        now

          let o be object;

          assume o in ( rng f);

          then

          consider k be object such that

           E: k in ( dom f) & o = (f . k) by FUNCT_1:def 3;

          (f . k) = ( 1. R) by E, D;

          hence o in the carrier of R by E;

        end;

        then ( rng f) c= the carrier of R;

        then

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

        now

          let k be Element of NAT ;

          assume 1 <= k & k <= n1;

          then

           E: k in ( dom f) by D, FINSEQ_3: 25;

          

          hence (f /. k) = (f . k) by PARTFUN1:def 6

          .= ( 1. R) by E, D;

        end;

        

        then

         E: ( Sum f) = (n1 * ( 1. R)) by D, POLYNOM8: 4

        .= ( - ( 1. R)) by F, RING_3:def 2;

        now

          let k be Nat;

          assume

           G: k in ( dom f);

          ( 1. R) is square;

          hence ex a be Element of R st (f . k) = (a ^2 ) by G, D;

        end;

        then ( - ( 1. R)) is sum_of_squares by E;

        then ( - ( 1. R)) in ( QS R);

        then ( - ( - ( 1. R))) in ( - P) by B;

        then ( 1. R) in (P /\ ( - P)) by A, XBOOLE_0:def 4;

        then ( 1. R) in {( 0. R)} by defppc;

        hence contradiction by TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: REALALG1:29

    

     ordsub: for R be ordered Ring holds for O,P be Ordering of R st O c= P holds O = P

    proof

      let R be ordered Ring, O,P be Ordering of R;

      assume

       AS: O c= P;

      now

        assume not (P c= O);

        then

        consider a be Element of R such that

         A: a in P & not (a in O);

        a in the carrier of R;

        then a in (O \/ ( - O)) by defsp;

        then a in ( - O) by A, XBOOLE_0:def 3;

        then

         B: ( - a) in ( - ( - O));

        ( - a) in ( - P) by A;

        then ( - a) in (P /\ ( - P)) by AS, B, XBOOLE_0:def 4;

        then ( - a) in {( 0. R)} by defneg;

        then

         C: ( - a) = ( 0. R) by TARSKI:def 1;

        a = ( - ( - a))

        .= ( 0. R) by C;

        hence contradiction by A, ord3;

      end;

      hence thesis by AS;

    end;

    begin

    definition

      let R be preordered Ring, P be Preordering of R;

      let a,b be Element of R;

      :: REALALG1:def18

      pred a <= P,b means (b - a) in P;

    end

    definition

      let R be preordered Ring, P be Preordering of R;

      :: REALALG1:def19

      func OrdRel P -> Relation of R equals { [a, b] where a,b be Element of R : a <= (P,b) };

      coherence

      proof

        set M = { [a, b] where a,b be Element of R : a <= (P,b) };

        M c= [:the carrier of R, the carrier of R:]

        proof

          let x be object;

          assume x in M;

          then

          consider a,b be Element of R such that

           A1: x = [a, b] & a <= (P,b);

          thus x in [:the carrier of R, the carrier of R:] by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be preordered Ring;

      let P be Preordering of R;

      cluster ( OrdRel P) -> non empty;

      coherence

      proof

        ( 0. R) <= (P,( 0. R)) by ord3;

        then [( 0. R), ( 0. R)] in { [a, b] where a,b be Element of R : a <= (P,b) };

        hence thesis;

      end;

    end

    registration

      let R be preordered Ring, P be Preordering of R;

      cluster ( OrdRel P) -> strongly_reflexive antisymmetric transitive;

      coherence

      proof

        set H = ( OrdRel P);

        now

          let x be object;

          assume x in the carrier of R;

          then

          reconsider a = x as Element of R;

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

          then a <= (P,a) by ord3;

          hence [x, x] in H;

        end;

        hence H is strongly_reflexive by RELAT_2:def 1;

        now

          let x,y be object;

          assume

           AS: x in ( field H) & y in ( field H) & [x, y] in H & [y, x] in H;

          then

          consider a,b be Element of R such that

           A1: [x, y] = [a, b] & a <= (P,b);

          consider e,f be Element of R such that

           A2: [e, f] = [y, x] & e <= (P,f) by AS;

          

           C: x = a & y = b & y = e & x = f by A1, A2, XTUPLE_0: 1;

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

          then (a - b) in ( - P) by A1;

          then (a - b) in (P /\ ( - P)) by C, A2, XBOOLE_0:def 4;

          then (a - b) in {( 0. R)} by defneg;

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

          hence x = y by C, RLVECT_1: 21;

        end;

        hence H is antisymmetric by RELAT_2:def 12, RELAT_2:def 4;

        now

          let x,y,z be object;

          assume

           AS: x in ( field H) & y in ( field H) & z in ( field H) & [x, y] in H & [y, z] in H;

          then

          consider a,b be Element of R such that

           A1: [x, y] = [a, b] & a <= (P,b);

          consider e,c be Element of R such that

           A2: [e, c] = [y, z] & e <= (P,c) by AS;

          

           C: x = a & y = b & y = e & z = c by A1, A2, XTUPLE_0: 1;

          then ((c - b) + (b - a)) in { (s1 + s2) where s1,s2 be Element of R : s1 in P & s2 in P } by A1, A2;

          then

           D: ((c - b) + (b - a)) in (P + P) by IDEAL_1:def 19;

          

           B: (P + P) c= P by defppc;

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

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

          .= ((c + ( 0. R)) + ( - a)) by RLVECT_1: 5

          .= (c - a);

          then a <= (P,c) by B, D;

          hence [x, z] in H by C;

        end;

        hence H is transitive by RELAT_2:def 16, RELAT_2:def 8;

      end;

    end

    registration

      let R be preordered Ring, P be Preordering of R;

      cluster ( OrdRel P) -> respecting_addition respecting_multiplication;

      coherence

      proof

        set Q = ( OrdRel P);

        now

          let r1,r2,r3 be Element of R;

          assume r1 <=_ (Q,r2);

          then

          consider a,b be Element of R such that

           A: [a, b] = [r1, r2] & a <= (P,b);

          

           B: a = r1 & b = r2 by A, XTUPLE_0: 1;

          ((r2 + r3) - (r1 + r3)) = ((r2 + r3) + (( - r3) + ( - r1))) by RLVECT_1: 31

          .= (((r2 + r3) + ( - r3)) + ( - r1)) by RLVECT_1:def 3

          .= ((r2 + (r3 + ( - r3))) + ( - r1)) by RLVECT_1:def 3

          .= ((r2 + ( 0. R)) + ( - r1)) by RLVECT_1: 5

          .= (r2 - r1);

          then (r1 + r3) <= (P,(r2 + r3)) by A, B;

          hence (r1 + r3) <=_ (Q,(r2 + r3));

        end;

        hence Q is respecting_addition;

        let r1,r2,r3 be Element of R;

        assume

         H: r1 <=_ (Q,r2) & ( 0. R) <=_ (Q,r3);

        then

        consider a,b be Element of R such that

         A: [a, b] = [r1, r2] & a <= (P,b);

        consider e,f be Element of R such that

         B: [e, f] = [( 0. R), r3] & e <= (P,f) by H;

        

         D: r1 = a & r2 = b & e = ( 0. R) & r3 = f by A, B, XTUPLE_0: 1;

        ((r2 * r3) - (r1 * r3)) = ((r2 - r1) * r3) by VECTSP_1: 13;

        then

         E: ((r2 * r3) - (r1 * r3)) in (P * P) by D, B, A;

        (P * P) c= P by defppc;

        then (r1 * r3) <= (P,(r2 * r3)) by E;

        hence (r1 * r3) <=_ (Q,(r2 * r3));

      end;

    end

    registration

      let R be ordered Ring, O be Ordering of R;

      cluster ( OrdRel O) -> totally_connected;

      coherence

      proof

        set H = ( OrdRel O);

        now

          let x,y be object;

          assume x in the carrier of R & y in the carrier of R;

          then

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

          

           A: (O \/ ( - O)) = the carrier of R by defpc;

          per cases by A, XBOOLE_0:def 3;

            suppose (a - b) in O;

            then b <= (O,a);

            hence [x, y] in H or [y, x] in H;

          end;

            suppose (a - b) in ( - O);

            then ( - (a - b)) in ( - ( - O));

            then a <= (O,b) by RLVECT_1: 33;

            hence [x, y] in H or [y, x] in H;

          end;

        end;

        hence thesis by RELAT_2:def 7;

      end;

    end

    registration

      let R be preordered Ring;

      cluster strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication for Relation of R;

      existence

      proof

        set P = the Preordering of R;

        take ( OrdRel P);

        thus thesis;

      end;

    end

    registration

      let R be ordered Ring;

      cluster strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication totally_connected for Relation of R;

      existence

      proof

        set P = the Ordering of R;

        take ( OrdRel P);

        thus thesis;

      end;

    end

    definition

      let R be preordered Ring;

      mode OrderRelation of R is strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication Relation of R;

    end

    definition

      let R be ordered Ring;

      mode total_OrderRelation of R is strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication totally_connected Relation of R;

    end

    definition

      let R be Ring;

      let Q be Relation of R;

      :: REALALG1:def20

      func Positives Q -> Subset of R equals { a where a be Element of R : ( 0. R) <=_ (Q,a) };

      coherence

      proof

        set M = { a where a be Element of R : ( 0. R) <=_ (Q,a) };

        M c= the carrier of R

        proof

          let x be object;

          assume x in M;

          then

          consider a be Element of R such that

           A1: x = a & ( 0. R) <=_ (Q,a);

          thus x in the carrier of R by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let R be preordered Ring;

      let Q be strongly_reflexive Relation of R;

      cluster ( Positives Q) -> non empty;

      coherence

      proof

        ( 0. R) <=_ (Q,( 0. R)) by defstr, RELAT_2:def 1;

        then ( 0. R) in ( Positives Q);

        hence thesis;

      end;

    end

    registration

      let R be preordered Ring;

      let Q be OrderRelation of R;

      cluster ( Positives Q) -> add-closed mult-closed negative-disjoint;

      coherence

      proof

        set P = ( Positives Q);

        now

          let x,y be Element of R;

          assume

           A0: x in P & y in P;

          then

          consider a be Element of R such that

           A1: x = a & ( 0. R) <=_ (Q,a);

          consider b be Element of R such that

           A2: y = b & ( 0. R) <=_ (Q,b) by A0;

          (( 0. R) + b) <=_ (Q,(a + b)) by respadd, A1;

          then ( 0. R) <=_ (Q,(a + b)) by A2, lemtrans;

          hence (x + y) in P by A1, A2;

        end;

        hence P is add-closed;

        now

          let x,y be Element of R;

          assume

           A0: x in P & y in P;

          then

          consider a be Element of R such that

           A1: x = a & ( 0. R) <=_ (Q,a);

          consider b be Element of R such that

           A2: y = b & ( 0. R) <=_ (Q,b) by A0;

          (( 0. R) * b) <=_ (Q,(a * b)) by respmult, A1, A2;

          hence (x * y) in P by A1, A2;

        end;

        hence P is mult-closed;

         A:

        now

          let x be object;

          assume x in (P /\ ( - P));

          then

           A0: x in P & x in ( - P) by XBOOLE_0:def 4;

          consider a be Element of R such that

           A1: x = a & ( 0. R) <=_ (Q,a) by A0;

          consider b be Element of R such that

           A2: x = ( - b) & b in P by A0;

          consider c be Element of R such that

           A3: c = b & ( 0. R) <=_ (Q,c) by A2;

          (a + ( 0. R)) <=_ (Q,(a + ( - a))) by A3, respadd, A1, A2;

          then a <=_ (Q,( 0. R)) by RLVECT_1: 5;

          then a = ( 0. R) by A1, lemanti;

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

        end;

        now

          let x be object;

          assume

           C: x in {( 0. R)};

          then

           A: x = ( 0. R) by TARSKI:def 1;

          reconsider a = x as Element of R by C;

          a <=_ (Q,a) by defstr, RELAT_2:def 1;

          then

           B: a in P by A;

          ( - a) = a by A;

          then a in ( - P) by B;

          hence x in (P /\ ( - P)) by B, XBOOLE_0:def 4;

        end;

        hence P is negative-disjoint by A, TARSKI: 2;

      end;

    end

    registration

      let R be ordered Ring;

      let Q be total_OrderRelation of R;

      cluster ( Positives Q) -> spanning;

      coherence

      proof

        set P = ( Positives Q);

         A:

        now

          let x be object;

          assume x in the carrier of R;

          then

          reconsider a = x as Element of R;

          per cases by Rtot, RELAT_2:def 7;

            suppose ( 0. R) <=_ (Q,a);

            then a in P;

            hence x in (P \/ ( - P)) by XBOOLE_0:def 3;

          end;

            suppose a <=_ (Q,( 0. R));

            then (a + ( - a)) <=_ (Q,(( 0. R) + ( - a))) by respadd;

            then ( 0. R) <=_ (Q,(( 0. R) + ( - a))) by RLVECT_1: 5;

            then ( - a) in P;

            then ( - ( - a)) in ( - P);

            hence x in (P \/ ( - P)) by XBOOLE_0:def 3;

          end;

        end;

        for x be object st x in (P \/ ( - P)) holds x in the carrier of R;

        hence thesis by A, TARSKI: 2;

      end;

    end

    theorem :: REALALG1:30

    for R be preordered Ring holds for P be Preordering of R holds ( OrdRel P) is OrderRelation of R;

    theorem :: REALALG1:31

    for R be ordered Ring holds for P be Ordering of R holds ( OrdRel P) is total_OrderRelation of R;

    theorem :: REALALG1:32

    for R be ordered Ring holds for Q be total_OrderRelation of R holds ( Positives Q) is Ordering of R;

    begin

    

     lemsubpreord: for R be preordered Ring, P be Preordering of R holds for S be Subring of R, Q be Subset of S st Q = (P /\ the carrier of S) holds Q is prepositive_cone

    proof

      let R be preordered Ring, P be Preordering of R, S be Subring of R, Q be Subset of S;

      assume

       AS: Q = (P /\ the carrier of S);

      now

        let o be object;

        assume

         A: o in Q;

        the carrier of S c= the carrier of R by C0SP1:def 3;

        hence o in the carrier of R by A;

      end;

      then

      reconsider Q1 = Q as Subset of R by TARSKI:def 3;

      

       AS1: ( - Q1) = ( - Q) by lemminus1;

      

       AS4: the carrier of S c= the carrier of R by C0SP1:def 3;

      reconsider E = the carrier of S as Subset of R by C0SP1:def 3;

       AS3:

      now

        let o be object;

        assume o in the carrier of S;

        then

        reconsider a = o as Element of S;

        reconsider b = ( - a) as Element of R by AS4;

        ( - b) = ( - ( - a)) by lemminus

        .= o;

        hence o in ( - E);

      end;

      now

        let o be object;

        assume o in ( - E);

        then

        consider a be Element of R such that

         B: ( - a) = o & a in E;

        reconsider b = a as Element of S by B;

        ( - a) = ( - b) by lemminus;

        hence o in the carrier of S by B;

      end;

      then

       AS2: the carrier of S = ( - E) by AS3, TARSKI: 2;

      

       A: (Q + Q) c= Q

      proof

        let x be object;

        assume x in (Q + Q);

        then x in { (a + b) where a,b be Element of S : a in Q & b in Q } by IDEAL_1:def 19;

        then

        consider a,b be Element of S such that

         A1: x = (a + b) & a in Q & b in Q;

        

         A2: a in P & b in P by A1, AS, XBOOLE_0:def 4;

        reconsider a1 = a, b1 = b as Element of R by A1, AS;

        (a1 + b1) in { (u + v) where u,v be Element of R : u in P & v in P } by A2;

        then

         A3: (a1 + b1) in (P + P) by IDEAL_1:def 19;

        

         A4: (P + P) c= P by defppc;

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

        then

         A6: [a, b] in ( dom the addF of S);

        (a1 + b1) = ((the addF of R || the carrier of S) . (a,b)) by A6, FUNCT_1: 49

        .= (a + b) by C0SP1:def 3;

        hence x in Q by A1, AS, A4, A3, XBOOLE_0:def 4;

      end;

      

       B: (Q * Q) c= Q

      proof

        let x be object;

        assume x in (Q * Q);

        then

        consider a,b be Element of S such that

         B1: x = (a * b) & a in Q & b in Q;

        

         B2: a in P & b in P by B1, AS, XBOOLE_0:def 4;

        reconsider a1 = a, b1 = b as Element of R by B1, AS;

        

         B3: (a1 * b1) in (P * P) by B2;

        

         B4: (P * P) c= P by defppc;

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

        then

         B6: [a, b] in ( dom the multF of S);

        (a1 * b1) = ((the multF of R || the carrier of S) . (a,b)) by B6, FUNCT_1: 49

        .= (a * b) by C0SP1:def 3;

        hence x in Q by B1, AS, B4, B3, XBOOLE_0:def 4;

      end;

       C1:

      now

        let o be object;

        assume o in (Q /\ ( - Q));

        then

         C3: o in Q & o in ( - Q) by XBOOLE_0:def 4;

        then o in ( - (P /\ the carrier of S)) by AS, lemminus1;

        then o in (( - P) /\ ( - E)) by min1;

        then o in P & o in ( - P) by C3, AS, XBOOLE_0:def 4;

        then

         C2: o in (P /\ ( - P)) by XBOOLE_0:def 4;

        (P /\ ( - P)) = {( 0. R)} by defppc;

        hence o in {( 0. S)} by C2, C0SP1:def 3;

      end;

       C:

      now

        let o be object;

        assume

         CC: o in {( 0. S)};

        

        then o = ( 0. S) by TARSKI:def 1

        .= ( 0. R) by C0SP1:def 3;

        then o in {( 0. R)} by TARSKI:def 1;

        then o in (P /\ ( - P)) by defppc;

        then

         C2: o in P & o in ( - P) by XBOOLE_0:def 4;

        then

         C5: o in Q by CC, AS, XBOOLE_0:def 4;

        o in (( - P) /\ ( - E)) by AS2, C2, CC, XBOOLE_0:def 4;

        then o in ( - (P /\ the carrier of S)) by min1;

        hence o in (Q /\ ( - Q)) by AS1, AS, C5, XBOOLE_0:def 4;

      end;

      

       Q: ( SQ S) c= ( SQ R) by SQsub;

      ( SQ R) c= P by defppc;

      then ( SQ S) c= P by Q;

      then ( SQ S) c= (P /\ the carrier of S) by XBOOLE_0:def 4;

      hence thesis by A, B, C, C1, AS, TARSKI: 2;

    end;

    

     lemsubord: for R be ordered Ring, O be Ordering of R holds for S be Subring of R, Q be Subset of S st Q = (O /\ the carrier of S) holds Q is positive_cone

    proof

      let R be ordered Ring, O be Ordering of R, S be Subring of R, Q be Subset of S;

      assume

       AS: Q = (O /\ the carrier of S);

      then

       AS1: Q is prepositive_cone by lemsubpreord;

      

       AS4: the carrier of S c= the carrier of R by C0SP1:def 3;

      reconsider E = the carrier of S as Subset of R by C0SP1:def 3;

       AS3:

      now

        let o be object;

        assume o in the carrier of S;

        then

        reconsider a = o as Element of S;

        reconsider b = ( - a) as Element of R by AS4;

        ( - b) = ( - ( - a)) by lemminus

        .= o;

        hence o in ( - E);

      end;

      now

        let o be object;

        assume o in ( - E);

        then

        consider a be Element of R such that

         B: ( - a) = o & a in E;

        reconsider b = a as Element of S by B;

        ( - a) = ( - b) by lemminus;

        hence o in the carrier of S by B;

      end;

      then

       AS2: the carrier of S = ( - E) by AS3, TARSKI: 2;

       B:

      now

        let o be object;

        assume

         A0: o in the carrier of S;

        then

        reconsider a = o as Element of R by AS4;

        

         A1: O is spanning;

        per cases by A1, XBOOLE_0:def 3;

          suppose a in O;

          then a in (O /\ the carrier of S) by A0, XBOOLE_0:def 4;

          hence o in (Q \/ ( - Q)) by AS, XBOOLE_0:def 3;

        end;

          suppose a in ( - O);

          then a in (( - O) /\ ( - E)) by AS2, A0, XBOOLE_0:def 4;

          then o in ( - (O /\ the carrier of S)) by min1;

          then o in ( - Q) by AS, lemminus1;

          hence o in (Q \/ ( - Q)) by XBOOLE_0:def 3;

        end;

      end;

      for o be object st o in (Q \/ ( - Q)) holds o in the carrier of S;

      hence thesis by AS1, B, TARSKI: 2;

    end;

    registration

      let R be preordered Ring;

      cluster -> preordered for Subring of R;

      coherence

      proof

        let S be Subring of R;

        set P = the Preordering of R;

        for o be object st o in (P /\ the carrier of S) holds o in the carrier of S by XBOOLE_0:def 4;

        then

        reconsider M = (P /\ the carrier of S) as Subset of S by TARSKI:def 3;

        M is prepositive_cone by lemsubpreord;

        hence thesis;

      end;

    end

    registration

      let R be ordered Ring;

      cluster -> ordered for Subring of R;

      coherence

      proof

        let S be Subring of R;

        set P = the Ordering of R;

        for o be object st o in (P /\ the carrier of S) holds o in the carrier of S by XBOOLE_0:def 4;

        then

        reconsider M = (P /\ the carrier of S) as Subset of S by TARSKI:def 3;

        M is positive_cone by lemsubord;

        hence thesis;

      end;

    end

    theorem :: REALALG1:33

    for R be preordered Ring holds for P be Preordering of R holds for S be Subring of R holds (P /\ the carrier of S) is Preordering of S

    proof

      let R be preordered Ring, O be Preordering of R, S be Subring of R;

      for o be object st o in (O /\ the carrier of S) holds o in the carrier of S by XBOOLE_0:def 4;

      then

      reconsider M = (O /\ the carrier of S) as Subset of S by TARSKI:def 3;

      M is prepositive_cone by lemsubpreord;

      hence thesis;

    end;

    theorem :: REALALG1:34

    for R be ordered Ring holds for O be Ordering of R holds for S be Subring of R holds (O /\ the carrier of S) is Ordering of S

    proof

      let R be ordered Ring, O be Ordering of R, S be Subring of R;

      for o be object st o in (O /\ the carrier of S) holds o in the carrier of S by XBOOLE_0:def 4;

      then

      reconsider M = (O /\ the carrier of S) as Subset of S by TARSKI:def 3;

      M is positive_cone by lemsubord;

      hence thesis;

    end;

    registration

      cluster F_Complex -> non preordered;

      coherence

      proof

        assume F_Complex is preordered;

        then

        reconsider F = F_Complex as preordered Field;

        consider P be Subset of F such that

         A1: P is prepositive_cone by defpord;

        reconsider P as Preordering of F by A1;

        reconsider i = <i> as Element of F by COMPLFLD:def 1;

        

         A2: ( QS F) c= P by ord2;

        ( - ( 1. F)) = ( - 1r ) by COMPLFLD: 2, COMPLFLD: 8

        .= ( <i> * <i> )

        .= (i ^2 ) by COMPLFLD: 4;

        then ( - ( 1. F)) is square;

        then ( - ( 1. F)) in ( QS F);

        hence contradiction by A2, ord4;

      end;

    end

    registration

      let n be non trivial Nat;

      cluster ( Z/ n) -> non preordered;

      coherence

      proof

        ( Char ( Z/ n)) <> 0 ;

        hence thesis by tchar;

      end;

    end

    definition

      :: REALALG1:def21

      func Positives(F_Real) -> Subset of F_Real equals { r where r be Element of REAL : 0 <= r };

      coherence

      proof

        now

          let o be object;

          assume o in { x where x be Element of REAL : 0 <= x };

          then

          consider x be Element of F_Real such that

           A: o = x & 0 <= x;

          thus o in the carrier of F_Real by A;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      cluster Positives(F_Real) -> add-closed mult-closed negative-disjoint spanning;

      coherence

      proof

         Positives(F_Real) is positive_cone by lemEX;

        hence thesis;

      end;

    end

    registration

      cluster F_Real -> ordered;

      coherence

      proof

         Positives(F_Real) is positive_cone;

        hence thesis;

      end;

    end

    theorem :: REALALG1:35

     Positives(F_Real) is Ordering of F_Real ;

    theorem :: REALALG1:36

    for O be Ordering of F_Real holds O = Positives(F_Real)

    proof

      let O be Ordering of F_Real ;

      

       X: ( QS F_Real ) c= O by ord2;

      now

        let x be object;

        assume x in Positives(F_Real) ;

        then

        consider r be Element of F_Real such that

         A: x = r & 0 <= r;

        reconsider q = ( sqrt r) as Element of F_Real by XREAL_0:def 1;

        r = (( sqrt r) ^2 ) by A, SQUARE_1:def 2

        .= (q ^2 );

        then r is square;

        then r in ( QS F_Real );

        hence x in O by A, X;

      end;

      then Positives(F_Real) c= O;

      hence thesis by ordsub;

    end;

    definition

      :: REALALG1:def22

      func Positives(F_Rat) -> Subset of F_Rat equals { r where r be Element of RAT : 0 <= r };

      coherence

      proof

        now

          let o be object;

          assume o in { x where x be Element of RAT : 0 <= x };

          then

          consider x be Element of RAT such that

           A: o = x & 0 <= x;

          thus o in the carrier of F_Rat by A, GAUSSINT:def 14;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      cluster Positives(F_Rat) -> add-closed mult-closed negative-disjoint spanning;

      coherence

      proof

        set S = Positives(F_Rat) ;

        set R = F_Rat ;

        

         A: (S + S) c= S

        proof

          let o be object;

          assume o in (S + S);

          then o in { (a + b) where a,b be Element of R : a in S & b in S } by IDEAL_1:def 19;

          then

          consider a,b be Element of R such that

           A: o = (a + b) & a in S & b in S;

          consider x be Element of RAT such that

           B: x = a & 0 <= x by A;

          consider y be Element of RAT such that

           C: y = b & 0 <= y by A;

          thus o in S by A, B, C, GAUSSINT:def 14;

        end;

        

         B: (S * S) c= S

        proof

          let o be object;

          assume o in (S * S);

          then

          consider a,b be Element of R such that

           A: o = (a * b) & a in S & b in S;

          consider x be Element of RAT such that

           B: x = a & 0 <= x by A;

          consider y be Element of RAT such that

           C: y = b & 0 <= y by A;

          thus o in S by A, B, C, GAUSSINT:def 14;

        end;

         K:

        now

          let o be object;

          assume

           K0: o in (S /\ ( - S));

          then

           K1: o in S & o in ( - S) by XBOOLE_0:def 4;

          reconsider x = o as Element of F_Rat by K0;

          consider y1 be Element of RAT such that

           K2: y1 = o & 0 <= y1 by K1;

          consider y2 be Element of F_Rat such that

           K3: ( - y2) = o & y2 in S by K1;

          reconsider y2 as Element of RAT by GAUSSINT:def 14;

          consider y be Element of RAT such that

           K4: y2 = y & 0 <= y by K3;

          y1 = ( 0. R) by K4, K2, K3, GAUSSINT:def 14;

          hence o in {( 0. R)} by K2, TARSKI:def 1;

        end;

         C:

        now

          let o be object;

          assume

           K0: o in {( 0. R)};

          then

           K1: o = ( 0. R) by TARSKI:def 1;

          reconsider x = o as Element of RAT by K0, GAUSSINT:def 14;

          reconsider xx = x as Element of R by GAUSSINT:def 14;

          

           K3: x in S by K0, GAUSSINT:def 14;

          ( - xx) in { ( - s) where s be Element of R : s in S } by K3;

          hence o in (S /\ ( - S)) by K1, K3, XBOOLE_0:def 4;

        end;

         F:

        now

          let o be object;

          assume o in the carrier of R;

          then

          reconsider x = o as Element of RAT by GAUSSINT:def 14;

          

           F1: ( - x) is Element of RAT by RAT_1:def 2;

          reconsider xx = x as Element of F_Rat by GAUSSINT:def 14;

          per cases ;

            suppose 0 <= x;

            then x in S;

            hence o in (S \/ ( - S)) by XBOOLE_0:def 3;

          end;

            suppose 0 <= ( - x);

            then ( - xx) in S by F1;

            then ( - ( - xx)) in ( - S);

            hence o in (S \/ ( - S)) by XBOOLE_0:def 3;

          end;

        end;

        for o be object st o in (S \/ ( - S)) holds o in the carrier of R;

        then S is positive_cone by A, B, C, K, F, TARSKI: 2;

        hence thesis;

      end;

    end

    registration

      cluster F_Rat -> ordered;

      coherence

      proof

         Positives(F_Rat) is positive_cone;

        hence thesis;

      end;

    end

    theorem :: REALALG1:37

     Positives(F_Rat) is Ordering of F_Rat ;

    theorem :: REALALG1:38

    for O be Ordering of F_Rat holds O = Positives(F_Rat)

    proof

      let O be Ordering of F_Rat ;

      defpred P[ Nat] means $1 in O;

      

       A: ( 0. F_Rat ) = 0 & ( 1. F_Rat ) = 1 by GAUSSINT:def 14;

      

       B: ( 1. F_Rat ) in O & ( 0. F_Rat ) in O by ord3;

      

       IA: P[ 0 ] by A, ord3;

      

       E: (O + O) c= O & (O * O) c= O by defpc;

       IS:

      now

        let k be Nat;

        assume

         C: P[k];

        then

        consider a be Element of F_Rat such that

         D: a = k;

        (a + ( 1. F_Rat )) in { (x + y) where x,y be Element of F_Rat : x in O & y in O } by D, C, B;

        then (k + 1) in (O + O) by GAUSSINT:def 14, D, IDEAL_1:def 19;

        hence P[(k + 1)] by E;

      end;

      

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

       Positives(F_Rat) c= O

      proof

        let o be object;

        assume o in Positives(F_Rat) ;

        then

        consider r be Element of RAT such that

         A1: o = r & 0 <= r;

        consider m,n be Integer such that

         B1: n <> 0 & r = (m / n) by RAT_1: 1;

        reconsider a = n, b = m as Element of F_Rat by RAT_1:def 2, GAUSSINT:def 14;

        per cases ;

          suppose m = 0 ;

          hence o in O by B1, A1, A, ord3;

        end;

          suppose

           C1: 0 < m;

          then 0 <= n by A1, B1;

          then

          reconsider n1 = n, m1 = m as Element of NAT by C1, INT_1: 3;

          

           C: m1 in O & n1 in O by I;

          a is non zero by B1, GAUSSINT:def 14;

          then (a " ) in O by C, ord5;

          then (b * (a " )) in (O * O) by C;

          then (b * (a " )) in O by E;

          hence o in O by A1, B1, GAUSSINT:def 14, GAUSSINT: 15;

        end;

          suppose

           C1: m < 0 ;

          then 0 >= n by A1, B1;

          then

          reconsider n1 = ( - n), m1 = ( - m) as Element of NAT by C1, INT_1: 3;

          

           C: m1 in O & n1 in O by I;

          

           K: ( - a) <> ( 0. F_Rat ) by B1, GAUSSINT:def 14;

          ( - a) is non zero by B1, GAUSSINT:def 14;

          then (( - a) " ) in O by C, ord5;

          then

           F: (( - b) * (( - a) " )) in (O * O) by C;

          

           H: ( - (n " )) = ( - (a " )) by B1, GAUSSINT:def 14, GAUSSINT: 15;

          a <> ( 0. F_Rat ) by B1, GAUSSINT:def 14;

          

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

          .= (( - (a " )) * ( - a));

          then (( - a) " ) = ( - (a " )) by VECTSP_1:def 10, K;

          hence o in O by A1, B1, F, E, H;

        end;

      end;

      hence thesis by ordsub;

    end;

    definition

      :: REALALG1:def23

      func Positives(INT.Ring) -> Subset of INT.Ring equals { i where i be Element of INT : 0 <= i };

      coherence

      proof

        now

          let o be object;

          assume o in { x where x be Element of INT : 0 <= x };

          then

          consider x be Element of INT such that

           A: o = x & 0 <= x;

          thus o in the carrier of INT.Ring by A, INT_3:def 3;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      cluster Positives(INT.Ring) -> add-closed mult-closed negative-disjoint spanning;

      coherence

      proof

         B:

        now

          let o be object;

          assume o in Positives(INT.Ring) ;

          then

          consider i be Element of INT such that

           A1: o = i & 0 <= i;

          reconsider r = i as Element of RAT by RAT_1:def 2;

          r in { x where x be Element of RAT : 0 <= x } by A1;

          hence o in ( Positives(F_Rat) /\ the carrier of INT.Ring ) by A1, INT_3:def 3, XBOOLE_0:def 4;

        end;

        now

          let o be object;

          assume

           B1: o in ( Positives(F_Rat) /\ the carrier of INT.Ring );

          then o in Positives(F_Rat) & o in the carrier of INT.Ring by XBOOLE_0:def 4;

          then

          consider a be Element of RAT such that

           B2: o = a & 0 <= a;

          a is Element of INT by B1, B2, INT_3:def 3, XBOOLE_0:def 4;

          hence o in Positives(INT.Ring) by B2;

        end;

        then Positives(INT.Ring) is positive_cone by RING_3: 47, B, lemsubord, TARSKI: 2;

        hence thesis;

      end;

    end

    registration

      cluster INT.Ring -> ordered;

      coherence

      proof

         Positives(INT.Ring) is positive_cone;

        hence thesis;

      end;

    end

    theorem :: REALALG1:39

     Positives(INT.Ring) is Ordering of INT.Ring ;

    theorem :: REALALG1:40

    for O be Ordering of INT.Ring holds O = Positives(INT.Ring)

    proof

      let O be Ordering of INT.Ring ;

      defpred P[ Nat] means $1 in O;

      

       B: ( 1. INT.Ring ) in O & ( 0. INT.Ring ) in O by ord3;

      ( 0. INT.Ring ) = 0 & ( 1. INT.Ring ) = 1 by INT_3:def 3;

      then

       IA: P[ 0 ] by ord3;

      

       E: (O + O) c= O by defpc;

       IS:

      now

        let k be Nat;

        assume

         C: P[k];

        then

        consider a be Element of INT.Ring such that

         D: a = k;

        (a + ( 1. INT.Ring )) in { (x + y) where x,y be Element of INT.Ring : x in O & y in O } by D, C, B;

        then (k + 1) in (O + O) by INT_3:def 3, D, IDEAL_1:def 19;

        hence P[(k + 1)] by E;

      end;

      

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

      now

        let o be object;

        assume o in Positives(INT.Ring) ;

        then

        consider i be Element of INT such that

         A: o = i & 0 <= i;

        i is Element of NAT by A, INT_1: 3;

        hence o in O by A, I;

      end;

      then Positives(INT.Ring) c= O;

      hence thesis by ordsub;

    end;

    begin

    definition

      let R be preordered Ring;

      let P be Preordering of R;

      :: REALALG1:def24

      func Positives(Poly) P -> Subset of ( Polynom-Ring R) equals { p where p be Polynomial of R : ( LC p) in P };

      coherence

      proof

        now

          let o be object;

          assume o in { x where x be Polynomial of R : ( LC x) in P };

          then

          consider x be Polynomial of R such that

           A: o = x & ( LC x) in P;

          thus o in the carrier of ( Polynom-Ring R) by A, POLYNOM3:def 10;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    

     lemminuspoly: for R be Ring, a be Element of ( Polynom-Ring R), b be Polynomial of R st a = b holds ( - a) = ( - b)

    proof

      let R be Ring, a be Element of ( Polynom-Ring R), b be Polynomial of R;

      assume

       AS: a = b;

      set K = ( Polynom-Ring R);

      reconsider c = ( - b) as Element of ( Polynom-Ring R) by POLYNOM3:def 10;

      (a + c) = (b - b) by AS, POLYNOM3:def 10

      .= ( 0_. R) by POLYNOM3: 29

      .= ( 0. K) by POLYNOM3:def 10

      .= (a + ( - a)) by RLVECT_1: 5;

      hence thesis by RLVECT_1: 8;

    end;

    registration

      let R be preordered non degenerated Ring;

      let P be Preordering of R;

      cluster ( Positives(Poly) P) -> add-closed negative-disjoint;

      coherence

      proof

        set M = ( Positives(Poly) P), K = ( Polynom-Ring R);

        

         X1: (P + P) c= P & (P * P) c= P by defppc;

        now

          let x,y be Element of K;

          assume

           AS: x in M & y in M;

          then

          consider p be Polynomial of R such that

           A: x = p & ( LC p) in P;

          consider q be Polynomial of R such that

           B: y = q & ( LC q) in P by AS;

          (( LC p) + ( LC q)) in { (x + y) where x,y be Element of R : x in P & y in P } by A, B;

          then

           C: (( LC p) + ( LC q)) in (P + P) by IDEAL_1:def 19;

           D:

          now

            assume

             D1: (( LC p) + ( LC q)) = ( 0. R);

            then ( LC q) = ( - ( LC p)) by RLVECT_1: 6;

            then ( - ( - ( LC p))) in ( - P) by B;

            then ( LC p) in (P /\ ( - P)) by A, XBOOLE_0:def 4;

            then ( LC p) in {( 0. R)} by defppc;

            hence ( LC p) = ( 0. R) by TARSKI:def 1;

            hence ( LC q) = ( 0. R) by D1;

          end;

          ( LC (p + q)) in P

          proof

            per cases by XXREAL_0: 1;

              suppose

               AS: ( len p) = ( len q);

              then

               C0: ((p + q) . (( len p) -' 1)) = (( LC p) + ( LC q)) by NORMSP_1:def 2;

              

               C11: ( len p) is_at_least_length_of p & ( len p) is_at_least_length_of q by AS, ALGSEQ_1:def 3;

              

               C1: ( len (p + q)) = ( len p)

              proof

                now

                  let m be Nat;

                  assume

                   c13: m is_at_least_length_of (p + q);

                  thus ( len p) <= m

                  proof

                    assume

                     C14: m < ( len p);

                    then

                     C15: (( len p) - 1) = (( len p) -' 1) by NAT_1: 14, XREAL_1: 233;

                    m < ((( len p) - 1) + 1) by C14;

                    then p is zero by D, C0, c13, C15, NAT_1: 13;

                    hence contradiction by C14, POLYNOM4: 3;

                  end;

                end;

                hence thesis by C11, ALGSEQ_1:def 3, POLYNOM3: 24;

              end;

              ( LC (p + q)) = (( LC p) + ( LC q)) by C1, AS, NORMSP_1:def 2;

              hence thesis by C, X1;

            end;

              suppose

               AS: ( len p) < ( len q);

              

              then

               C11: ( len (p + q)) = ( max (( len p),( len q))) by POLYNOM4: 7

              .= ( len q) by AS, XXREAL_0:def 10;

              

               C15: (( len q) - 1) = (( len q) -' 1) by AS, NAT_1: 14, XREAL_1: 233;

              ( len p) < ((( len q) - 1) + 1) by AS;

              then

               C13: ( len p) <= (( len q) -' 1) by C15, NAT_1: 13;

              ( len p) is_at_least_length_of p by ALGSEQ_1:def 3;

              then

               C12: (p . (( len q) -' 1)) = ( 0. R) by C13;

              ( LC (p + q)) = ((p . (( len q) -' 1)) + (q . (( len q) -' 1))) by NORMSP_1:def 2, C11

              .= ( LC q) by C12;

              hence thesis by B;

            end;

              suppose

               AS: ( len p) > ( len q);

              

              then

               C11: ( len (p + q)) = ( max (( len p),( len q))) by POLYNOM4: 7

              .= ( len p) by AS, XXREAL_0:def 10;

              

               C15: (( len p) - 1) = (( len p) -' 1) by XREAL_1: 233, AS, NAT_1: 14;

              ( len q) < ((( len p) - 1) + 1) by AS;

              then

               C13: ( len q) <= (( len p) -' 1) by C15, NAT_1: 13;

              ( len q) is_at_least_length_of q by ALGSEQ_1:def 3;

              then

               C12: (q . (( len p) -' 1)) = ( 0. R) by C13;

              ( LC (p + q)) = ((p . (( len p) -' 1)) + (q . (( len p) -' 1))) by NORMSP_1:def 2, C11

              .= ( LC p) by C12;

              hence thesis by A;

            end;

          end;

          then (p + q) in { r where r be Polynomial of R : ( LC r) in P };

          hence (x + y) in M by A, B, POLYNOM3:def 10;

        end;

        hence M is add-closed;

         X:

        now

          let o be object;

          assume o in {( 0. K)};

          then o = ( 0. K) by TARSKI:def 1;

          then

           X1: o = ( 0_. R) by POLYNOM3:def 10;

          ( LC ( 0_. R)) = ( 0. R) by FUNCOP_1: 7;

          then ( LC ( 0_. R)) in {( 0. R)} by TARSKI:def 1;

          then ( LC ( 0_. R)) in (P /\ ( - P)) by defppc;

          then ( LC ( 0_. R)) in P & ( LC ( 0_. R)) in ( - P) by XBOOLE_0:def 4;

          then

           X3: ( 0_. R) in M;

          reconsider q = ( 0_. R) as Element of K by POLYNOM3:def 10;

          

           X4: ( - q) in { ( - p) where p be Element of K : p in M } by X3;

          ( len ( - ( 0_. R))) = ( len ( 0_. R)) by POLYNOM4: 8

          .= 0 by POLYNOM4: 3;

          

          then ( 0_. R) = ( - ( 0_. R)) by POLYNOM4: 5

          .= ( - q) by lemminuspoly;

          hence o in (M /\ ( - M)) by X1, X3, X4, XBOOLE_0:def 4;

        end;

        now

          let o be object;

          assume o in (M /\ ( - M));

          then

           X1: o in M & o in ( - M) by XBOOLE_0:def 4;

          then

          consider p be Polynomial of R such that

           X2: o = p & ( LC p) in P;

          consider x be Element of K such that

           X3: o = ( - x) & x in M by X1;

          consider q be Polynomial of R such that

           X4: x = q & ( LC q) in P by X3;

          

           X6: p = ( - q) by X4, X3, X2, lemminuspoly;

          then ( len p) = ( len q) by POLYNOM4: 8;

          then ( LC p) = ( - ( LC q)) by BHSP_1: 44, X6;

          then ( LC p) in ( - P) by X4;

          then ( LC p) in (P /\ ( - P)) by X2, XBOOLE_0:def 4;

          then ( LC p) in {( 0. R)} by defppc;

          then p is zero by TARSKI:def 1;

          then p = ( 0. K) by POLYNOM3:def 10;

          hence o in {( 0. K)} by X2, TARSKI:def 1;

        end;

        hence M is negative-disjoint by X, TARSKI: 2;

      end;

    end

    registration

      let R be preordered domRing;

      let P be Preordering of R;

      cluster ( Positives(Poly) P) -> mult-closed with_sums_of_squares;

      coherence

      proof

        set M = ( Positives(Poly) P), K = ( Polynom-Ring R);

        

         X: (P + P) c= P & (P * P) c= P & ( SQ R) c= P by defppc;

        now

          let x,y be Element of K;

          assume

           AS: x in M & y in M;

          then

          consider p be Polynomial of R such that

           A: x = p & ( LC p) in P;

          consider q be Polynomial of R such that

           B: y = q & ( LC q) in P by AS;

          

           C1: (( LC p) * ( LC q)) in (P * P) by A, B;

          per cases ;

            suppose p = ( 0_. R);

            then (p *' q) = ( 0_. R) by POLYNOM3: 34;

            then ( LC (p *' q)) = ( 0. R) by FUNCOP_1: 7;

            then ( LC (p *' q)) in P by ord3;

            then (p *' q) in { r where r be Polynomial of R : ( LC r) in P };

            hence (x * y) in M by A, B, POLYNOM3:def 10;

          end;

            suppose q = ( 0_. R);

            then (p *' q) = ( 0_. R) by POLYNOM4: 2;

            then ( LC (p *' q)) = ( 0. R) by FUNCOP_1: 7;

            then ( LC (p *' q)) in P by ord3;

            then (p *' q) in { r where r be Polynomial of R : ( LC r) in P };

            hence (x * y) in M by A, B, POLYNOM3:def 10;

          end;

            suppose

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

            then p is non zero & q is non zero;

            then ( LC p) <> ( 0. R) & ( LC q) <> ( 0. R);

            then ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. R) by VECTSP_2:def 1;

            then ( len (p *' q)) = ((( len p) + ( len q)) - 1) by POLYNOM4: 10;

            then ( LC (p *' q)) = (( LC p) * ( LC q)) by Z, lemmul;

            then (p *' q) in { r where r be Polynomial of R : ( LC r) in P } by C1, X;

            hence (x * y) in M by A, B, POLYNOM3:def 10;

          end;

        end;

        hence M is mult-closed;

        now

          let o be object;

          assume o in ( SQ K);

          then

          consider a be Element of K such that

           X1: o = a & a is square;

          reconsider p = a as Polynomial of R by POLYNOM3:def 10;

          consider b be Element of K such that

           X2: a = (b ^2 ) by X1;

          reconsider q = b as Polynomial of R by POLYNOM3:def 10;

          

           X3: p = (q *' q) by POLYNOM3:def 10, X2;

          per cases ;

            suppose q = ( 0_. R);

            then p = ( 0_. R) by X3, POLYNOM3: 34;

            then ( LC p) = ( 0. R) by FUNCOP_1: 7;

            then ( LC p) in P by ord3;

            hence o in M by X1;

          end;

            suppose

             Z: q <> ( 0_. R);

            then q is non zero;

            then ( LC q) <> ( 0. R);

            then ((q . (( len q) -' 1)) * (q . (( len q) -' 1))) <> ( 0. R) by VECTSP_2:def 1;

            then ( len (q *' q)) = ((( len q) + ( len q)) - 1) by POLYNOM4: 10;

            then ( LC (q *' q)) = (( LC q) ^2 ) by Z, lemmul;

            then ( LC (q *' q)) is square;

            then ( LC (q *' q)) in ( SQ R);

            hence o in M by X, X1, X3;

          end;

        end;

        then ( SQ K) c= M;

        then M is with_squares;

        hence M is with_sums_of_squares;

      end;

    end

    registration

      let R be ordered Ring;

      let O be Ordering of R;

      cluster ( Positives(Poly) O) -> spanning;

      coherence

      proof

        set P = ( Positives(Poly) O), K = ( Polynom-Ring R);

         X:

        now

          let o be object;

          assume o in the carrier of K;

          then

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

          

           X1: (O \/ ( - O)) = the carrier of R by defpc;

          per cases by X1, XBOOLE_0:def 3;

            suppose ( LC p) in O;

            then p in P;

            hence o in (P \/ ( - P)) by XBOOLE_0:def 3;

          end;

            suppose ( LC p) in ( - O);

            then

            consider a be Element of R such that

             A: ( - a) = ( LC p) & a in O;

            reconsider b = ( - p) as Element of K by POLYNOM3:def 10;

            ( LC ( - p)) = (( - p) . (( len p) -' 1)) by POLYNOM4: 8

            .= ( - (p . (( len p) -' 1))) by BHSP_1: 44

            .= a by A;

            then ( - p) in P by A;

            then

             C: ( - b) in ( - P);

            ( - b) = ( - ( - p)) by lemminuspoly

            .= p by HURWITZ: 10;

            hence o in (P \/ ( - P)) by C, XBOOLE_0:def 3;

          end;

        end;

        for o be object st o in (P \/ ( - P)) holds o in the carrier of K;

        hence thesis by X, TARSKI: 2;

      end;

    end

    registration

      let R be preordered domRing;

      cluster ( Polynom-Ring R) -> preordered;

      coherence

      proof

        set P = the Preordering of R;

        ( Positives(Poly) P) is prepositive_cone;

        hence thesis;

      end;

    end

    registration

      let R be ordered domRing;

      cluster ( Polynom-Ring R) -> ordered;

      coherence

      proof

        set P = the Ordering of R;

        ( Positives(Poly) P) is positive_cone;

        hence thesis;

      end;

    end

    theorem :: REALALG1:41

    for R be preordered domRing holds for P be Preordering of R holds ( Positives(Poly) P) is Preordering of ( Polynom-Ring R);

    theorem :: REALALG1:42

    for R be ordered domRing holds for O be Ordering of R holds ( Positives(Poly) O) is Ordering of ( Polynom-Ring R);

    definition

      let R be preordered Ring;

      let P be Preordering of R;

      :: REALALG1:def25

      func LowPositives(Poly) P -> Subset of ( Polynom-Ring R) equals { p where p be Polynomial of R : (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P };

      coherence

      proof

        set M = { p where p be Polynomial of R : (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P };

        now

          let x be object;

          assume x in M;

          then

          consider p be Polynomial of R such that

           H: x = p & (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P;

          thus x in the carrier of ( Polynom-Ring R) by H, POLYNOM3:def 10;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    

     lemlowp1: for R be preordered non degenerated Ring holds for P be Preordering of R holds for p,q be non zero Polynomial of R st (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P & (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) in P holds ((p + q) . ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) })) in P

    proof

      let R be preordered non degenerated Ring;

      let P be Preordering of R;

      let p,q be non zero Polynomial of R;

      assume

       AS: (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P & (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) in P;

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      

       Z1: (P + P) c= P & (P /\ ( - P)) = {( 0. R)} by defppc;

      now

        let o be object;

        assume o in { i where i be Nat : ((p + q) . i) <> ( 0. R) };

        then

        consider i be Nat such that

         H1: o = i & ((p + q) . i) <> ( 0. R);

        thus o in NAT by H1, ORDINAL1:def 12;

      end;

      then

      reconsider cpq = { i where i be Nat : ((p + q) . i) <> ( 0. R) } as Subset of NAT by TARSKI:def 3;

      per cases by XXREAL_0: 1;

        suppose

         AS1: ( min* cp) > ( min* cq);

         not (( min* cq) in cp) by AS1, NAT_1:def 1;

        then (p . ( min* cq)) = ( 0. R);

        then ((p + q) . ( min* cq)) = (( 0. R) + (q . ( min* cq))) by NORMSP_1:def 2;

        hence thesis by AS1, AS, lemlowp1a1;

      end;

        suppose

         AS1: ( min* cp) < ( min* cq);

         not (( min* cp) in cq) by AS1, NAT_1:def 1;

        then (q . ( min* cp)) = ( 0. R);

        then ((p + q) . ( min* cp)) = (( 0. R) + (p . ( min* cp))) by NORMSP_1:def 2;

        hence thesis by AS1, AS, lemlowp1a1;

      end;

        suppose

         XX: ( min* cp) = ( min* cq);

        then

         D1: ((p + q) . ( min* cp)) = ((p . ( min* cp)) + (q . ( min* cq))) by NORMSP_1:def 2;

        now

          assume ( 0. R) = ((p . ( min* cp)) + (q . ( min* cp)));

          then (p . ( min* cp)) = ( - (q . ( min* cp))) by RLVECT_1: 6;

          then (p . ( min* cp)) in ( - P) by AS, XX;

          then

           Y: (p . ( min* cp)) in (P /\ ( - P)) by AS, XBOOLE_0:def 4;

          ( min* cp) in cp by NAT_1:def 1;

          then

          consider w1 be Nat such that

           H2: w1 = ( min* cp) & (p . w1) <> ( 0. R);

          thus contradiction by Y, H2, Z1, TARSKI:def 1;

        end;

        

        then ( min* cpq) = ( min (( min* cp),( min* cq))) by XX, lemlowp1b

        .= ( min* cp) by XX;

        hence thesis by D1, AS, IDEAL_1:def 1;

      end;

    end;

    

     lemlowp3: for R be domRing, p,q be non zero Polynomial of R holds ((p *' q) . ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) })) = ((p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) * (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })))

    proof

      let R be domRing, p,q be non zero Polynomial of R;

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) }, cq = { i where i be Nat : (q . i) <> ( 0. R) }, cpq = { i where i be Nat : ((p *' q) . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      set m = (( min* cp) + ( min* cq));

      consider r be FinSequence of the carrier of R such that

       M: ( len r) = (m + 1) & ((p *' q) . m) = ( Sum r) & for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((m + 1) -' k))) by POLYNOM3:def 9;

      

       B1: 1 <= (( min* cp) + 1) by NAT_1: 11;

      (( min* cp) + 1) <= ((( min* cp) + 1) + ( min* cq)) by NAT_1: 11;

      then

       A1: (( min* cp) + 1) in ( dom r) by M, B1, FINSEQ_3: 25;

      

       A2: ((( min* cp) + 1) - 1) >= 0 ;

      

       A4: ((m + 1) -' (( min* cp) + 1)) = ((m + 1) - (( min* cp) + 1)) by XREAL_0:def 2;

      now

        let k be Element of NAT ;

        assume

         E: k in ( dom r) & k <> (( min* cp) + 1);

        then

         EE: 1 <= k <= (m + 1) by M, FINSEQ_3: 25;

        per cases by E, XXREAL_0: 1;

          suppose

           E1: k < (( min* cp) + 1);

          reconsider k1 = (k - 1) as Element of NAT by EE, INT_1: 3;

          

           E4: (k -' 1) = (k - 1) by EE, XREAL_0:def 2;

          then

           E3: (k -' 1) < ((( min* cp) + 1) - 1) by E1, XREAL_1: 9;

          now

            assume (p . k1) <> ( 0. R);

            then k1 in cp;

            hence contradiction by E3, E4, NAT_1:def 1;

          end;

          then (r . k) = (( 0. R) * (q . ((m + 1) -' k))) by E4, E, M;

          hence (r /. k) = ( 0. R) by E, PARTFUN1:def 6;

        end;

          suppose k > (( min* cp) + 1);

          then

           E1: ((m + 1) - k) < ((m + 1) - (( min* cp) + 1)) by XREAL_1: 10;

          ((m + 1) - k) in NAT by EE, INT_1: 5;

          then

           E3: ((m + 1) -' k) < ( min* cq) by E1, XREAL_0:def 2;

          now

            assume (q . ((m + 1) -' k)) <> ( 0. R);

            then ((m + 1) -' k) in cq;

            hence contradiction by E3, NAT_1:def 1;

          end;

          then (r . k) = ((p . (k -' 1)) * ( 0. R)) by E, M;

          hence (r /. k) = ( 0. R) by E, PARTFUN1:def 6;

        end;

      end;

      

      then ( Sum r) = (r /. (( min* cp) + 1)) by A1, POLYNOM2: 3

      .= (r . (( min* cp) + 1)) by A1, PARTFUN1:def 6

      .= ((p . ((( min* cp) + 1) -' 1)) * (q . ((m + 1) -' (( min* cp) + 1)))) by A1, M

      .= ((p . ( min* cp)) * (q . ( min* cq))) by A4, A2, XREAL_0:def 2;

      hence thesis by M, lemlowp3b;

    end;

    registration

      let R be preordered non degenerated Ring;

      let P be Preordering of R;

      cluster ( LowPositives(Poly) P) -> add-closed negative-disjoint;

      coherence

      proof

        set M = ( LowPositives(Poly) P), K = ( Polynom-Ring R);

        

         X2: ( 0. R) in P by ord3;

        now

          let x,y be Element of K;

          assume

           AS: x in M & y in M;

          then

          consider p be Polynomial of R such that

           H1: x = p & (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P;

          consider q be Polynomial of R such that

           H2: y = q & (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) in P by AS;

          per cases ;

            suppose

             A: p is zero;

            

             B: ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (q . i) <> ( 0. R) }) by lemlowp0, A;

            ((p + q) . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) = (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) by A, POLYNOM3: 28;

            then (p + q) in { r where r be Polynomial of R : (r . ( min* { i where i be Nat : (r . i) <> ( 0. R) })) in P } by B, H2;

            hence (x + y) in M by H1, H2, POLYNOM3:def 10;

          end;

            suppose

             A: q is zero;

            then

             B: ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) }) = ( min* { i where i be Nat : (p . i) <> ( 0. R) }) by lemlowp0;

            ((p + q) . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) = (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) by A, POLYNOM3: 28;

            then (p + q) in { r where r be Polynomial of R : (r . ( min* { i where i be Nat : (r . i) <> ( 0. R) })) in P } by B, H1;

            hence (x + y) in M by H1, H2, POLYNOM3:def 10;

          end;

            suppose p is non zero & q is non zero;

            then ((p + q) . ( min* { i where i be Nat : ((p + q) . i) <> ( 0. R) })) in P by H1, H2, lemlowp1;

            then (p + q) in { r where r be Polynomial of R : (r . ( min* { i where i be Nat : (r . i) <> ( 0. R) })) in P };

            hence (x + y) in M by H1, H2, POLYNOM3:def 10;

          end;

        end;

        hence M is add-closed;

         X:

        now

          let o be object;

          assume

           X00: o in {( 0. K)};

          then

           X0: o = ( 0. K) by TARSKI:def 1;

          then

           X1: o = ( 0_. R) by POLYNOM3:def 10;

          reconsider q = o as Polynomial of R by X00, POLYNOM3:def 10;

          (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) = ( 0. R) by X1, FUNCOP_1: 7;

          then

           X3: q in M by X2;

          reconsider q as Element of K by POLYNOM3:def 10;

          ( - q) in { ( - p) where p be Element of K : p in M } by X3;

          hence o in (M /\ ( - M)) by X0, X3, XBOOLE_0:def 4;

        end;

        now

          let o be object;

          assume o in (M /\ ( - M));

          then

           X1: o in M & o in ( - M) by XBOOLE_0:def 4;

          then

          consider p be Polynomial of R such that

           X2: o = p & (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P;

          set V = { i where i be Nat : (p . i) <> ( 0. R) };

          consider x be Element of K such that

           X3: o = ( - x) & x in M by X1;

          consider q be Polynomial of R such that

           X4: x = q & (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) in P by X3;

           X8:

          now

            let o be object;

            assume o in { i where i be Nat : (p . i) <> ( 0. R) };

            then

            consider i be Nat such that

             H1: o = i & (p . i) <> ( 0. R);

            thus o in NAT by H1, ORDINAL1:def 12;

          end;

          now

            assume { i where i be Nat : (p . i) <> ( 0. R) } <> {} ;

            then

            reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) } as non empty Subset of NAT by X8, TARSKI:def 3;

            ( min* cp) in cp by NAT_1:def 1;

            then

            consider i be Nat such that

             X9: i = ( min* cp) & (p . i) <> ( 0. R);

            

             X15: ( - ( - x)) = x;

            

            then

             X13: (q . i) = (( - p) . i) by X4, X3, X2, lemminuspoly

            .= ( - (p . i)) by BHSP_1: 44;

            now

              assume (q . i) = ( 0. R);

              then ( - ( - (p . i))) = ( - ( 0. R)) by X13;

              hence contradiction by X9;

            end;

            then

             X11: i in { i where i be Nat : (q . i) <> ( 0. R) };

            now

              let o be object;

              assume o in { i where i be Nat : (q . i) <> ( 0. R) };

              then

              consider i be Nat such that

               H1: o = i & (q . i) <> ( 0. R);

              thus o in NAT by H1, ORDINAL1:def 12;

            end;

            then

            reconsider cq = { i where i be Nat : (q . i) <> ( 0. R) } as non empty Subset of NAT by X11, TARSKI:def 3;

            now

              let k be Nat;

              assume k in { i where i be Nat : (q . i) <> ( 0. R) };

              then

              consider j be Nat such that

               X14: k = j & (q . j) <> ( 0. R);

              (q . j) = (( - p) . j) by X15, X4, X3, X2, lemminuspoly

              .= ( - (p . j)) by BHSP_1: 44;

              then (p . j) <> ( 0. R) by X14;

              then j in cp;

              hence i <= k by X14, X9, NAT_1:def 1;

            end;

            then ( min* cq) = i by X11, NAT_1:def 1;

            

            then (p . i) = (( - q) . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) by X4, X3, X2, lemminuspoly

            .= ( - (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) }))) by BHSP_1: 44;

            then (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in ( - P) by X4, X9;

            then (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in (P /\ ( - P)) by X2, XBOOLE_0:def 4;

            then (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in {( 0. R)} by defppc;

            hence contradiction by X9, TARSKI:def 1;

          end;

          

          then p = ( 0_. R) by lemlp0

          .= ( 0. K) by POLYNOM3:def 10;

          hence o in {( 0. K)} by X2, TARSKI:def 1;

        end;

        hence M is negative-disjoint by X, TARSKI: 2;

      end;

    end

    registration

      let R be preordered domRing;

      let P be Preordering of R;

      cluster ( LowPositives(Poly) P) -> mult-closed with_sums_of_squares;

      coherence

      proof

        set M = ( LowPositives(Poly) P), K = ( Polynom-Ring R);

        

         X: (P + P) c= P & (P * P) c= P & ( SQ R) c= P by defppc;

        now

          let x,y be Element of K;

          assume

           AS: x in M & y in M;

          then

          consider p be Polynomial of R such that

           A: x = p & (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P;

          consider q be Polynomial of R such that

           B: y = q & (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) in P by AS;

          

           C1: ((p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) * (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) }))) in (P * P) by A, B;

          per cases ;

            suppose p = ( 0_. R);

            then (p *' q) = ( 0_. R) by POLYNOM3: 34;

            then ((p *' q) . ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) })) = ( 0. R) by FUNCOP_1: 7;

            then ((p *' q) . ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) })) in P by ord3;

            then (p *' q) in { r where r be Polynomial of R : (r . ( min* { i where i be Nat : (r . i) <> ( 0. R) })) in P };

            hence (x * y) in M by A, B, POLYNOM3:def 10;

          end;

            suppose q = ( 0_. R);

            then (p *' q) = ( 0_. R) by POLYNOM4: 2;

            then ((p *' q) . ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) })) = ( 0. R) by FUNCOP_1: 7;

            then ((p *' q) . ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) })) in P by ord3;

            then (p *' q) in { r where r be Polynomial of R : (r . ( min* { i where i be Nat : (r . i) <> ( 0. R) })) in P };

            hence (x * y) in M by A, B, POLYNOM3:def 10;

          end;

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

            then p is non zero & q is non zero;

            then ((p *' q) . ( min* { i where i be Nat : ((p *' q) . i) <> ( 0. R) })) in (P * P) by C1, lemlowp3;

            then (p *' q) in { r where r be Polynomial of R : (r . ( min* { i where i be Nat : (r . i) <> ( 0. R) })) in P } by X;

            hence (x * y) in M by A, B, POLYNOM3:def 10;

          end;

        end;

        hence M is mult-closed;

        now

          let o be object;

          assume o in ( SQ K);

          then

          consider a be Element of K such that

           X1: o = a & a is square;

          reconsider p = a as Polynomial of R by POLYNOM3:def 10;

          consider b be Element of K such that

           X2: a = (b ^2 ) by X1;

          reconsider q = b as Polynomial of R by POLYNOM3:def 10;

          

           X3: p = (q *' q) by POLYNOM3:def 10, X2;

          per cases ;

            suppose q = ( 0_. R);

            then p = ( 0_. R) by X3, POLYNOM3: 34;

            then (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) = ( 0. R) by FUNCOP_1: 7;

            then (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in P by ord3;

            hence o in M by X1;

          end;

            suppose q <> ( 0_. R);

            then

            reconsider qq = q as non zero Polynomial of R by UPROOTS:def 5;

            ((q *' q) . ( min* { i where i be Nat : ((qq *' qq) . i) <> ( 0. R) })) = ((q . ( min* { i where i be Nat : (qq . i) <> ( 0. R) })) * (q . ( min* { i where i be Nat : (qq . i) <> ( 0. R) }))) by lemlowp3;

            then ((q *' q) . ( min* { i where i be Nat : ((q *' q) . i) <> ( 0. R) })) = ((q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) ^2 );

            then ((q *' q) . ( min* { i where i be Nat : ((q *' q) . i) <> ( 0. R) })) is square;

            then ((q *' q) . ( min* { i where i be Nat : ((q *' q) . i) <> ( 0. R) })) in ( SQ R);

            hence o in M by X, X1, X3;

          end;

        end;

        then ( SQ K) c= M;

        then M is with_squares;

        hence M is with_sums_of_squares;

      end;

    end

    registration

      let R be ordered non degenerated Ring;

      let O be Ordering of R;

      cluster ( LowPositives(Poly) O) -> spanning;

      coherence

      proof

        set P = ( LowPositives(Poly) O), K = ( Polynom-Ring R);

         X:

        now

          let o be object;

          assume o in the carrier of K;

          then

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

          

           X1: (O \/ ( - O)) = the carrier of R by defpc;

          per cases by X1, XBOOLE_0:def 3;

            suppose (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in O;

            then p in P;

            hence o in (P \/ ( - P)) by XBOOLE_0:def 3;

          end;

            suppose (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) in ( - O);

            then

            consider a be Element of R such that

             A: ( - a) = (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) })) & a in O;

            reconsider b = ( - p) as Element of K by POLYNOM3:def 10;

            (( - p) . ( min* { i where i be Nat : (( - p) . i) <> ( 0. R) })) = ( - (p . ( min* { i where i be Nat : (( - p) . i) <> ( 0. R) }))) by BHSP_1: 44

            .= ( - (p . ( min* { i where i be Nat : (p . i) <> ( 0. R) }))) by lemlowp2

            .= a by A;

            then ( - p) in P by A;

            then

             C: ( - b) in ( - P);

            ( - b) = ( - ( - p)) by lemminuspoly

            .= p by HURWITZ: 10;

            hence o in (P \/ ( - P)) by C, XBOOLE_0:def 3;

          end;

        end;

        for o be object st o in (P \/ ( - P)) holds o in the carrier of K;

        hence thesis by X, TARSKI: 2;

      end;

    end

    theorem :: REALALG1:43

    for R be preordered domRing holds for P be Preordering of R holds ( LowPositives(Poly) P) is Preordering of ( Polynom-Ring R);

    theorem :: REALALG1:44

    for R be ordered domRing holds for O be Ordering of R holds ( LowPositives(Poly) O) is Ordering of ( Polynom-Ring R);

    theorem :: REALALG1:45

    for R be preordered non degenerated Ring holds for P be Preordering of R holds ( Positives(Poly) P) <> ( LowPositives(Poly) P)

    proof

      let R be preordered non degenerated Ring, P be Preordering of R;

      set p = ( rpoly (1,( 1. R)));

      reconsider cp = { i where i be Nat : (p . i) <> ( 0. R) } as non empty Subset of NAT by lemlp1;

      ( deg p) = 1 by HURWITZ: 27;

      then (( len p) -' 1) = 1 by XREAL_0:def 2;

      then (p . (( len p) -' 1)) = ( 1_ R) by HURWITZ: 25;

      then

       B: ( LC p) = ( 1. R);

      

       A: ( 1. R) in P by ord3;

      

       E: (p . 0 ) = ( - (( power R) . (( 1. R),( 0 + 1)))) by HURWITZ: 25

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

      .= ( - (( 1_ R) * ( 1. R))) by GROUP_1:def 7

      .= ( - ( 1. R));

      now

        assume ( - ( 1. R)) = ( 0. R);

        then ( - ( - ( 1. R))) = ( 0. R);

        hence contradiction;

      end;

      then 0 in cp by E;

      then

       C: ( min* cp) = 0 by NAT_1:def 1;

      now

        assume p in ( LowPositives(Poly) P);

        then

        consider q be Polynomial of R such that

         H: q = p & (q . ( min* { i where i be Nat : (q . i) <> ( 0. R) })) in P;

        thus contradiction by H, C, E, ord4;

      end;

      hence thesis by A, B;

    end;