o_ring_1.miz



    begin

    reserve i,j,k,m,n for Nat;

    reserve R for non empty doubleLoopStr;

    reserve x,y for Scalar of R;

    reserve f,g,h for FinSequence of R;

    

     Lm1: h = (f ^ g) iff ( dom h) = ( Seg (( len f) + ( len g))) & (for k be Nat st k in ( dom f) holds (h /. k) = (f /. k)) & for k be Nat st k in ( dom g) holds (h /. (( len f) + k)) = (g /. k)

    proof

      

       A1: ( len f) >= 0 by NAT_1: 2;

      thus h = (f ^ g) implies ( dom h) = ( Seg (( len f) + ( len g))) & (for k be Nat st k in ( dom f) holds (h /. k) = (f /. k)) & for k be Nat st k in ( dom g) holds (h /. (( len f) + k)) = (g /. k)

      proof

        assume

         A2: h = (f ^ g);

        hence ( dom h) = ( Seg (( len f) + ( len g))) by FINSEQ_1:def 7;

        then

         A3: ( len h) = (( len f) + ( len g)) by FINSEQ_1:def 3;

        thus for k be Nat st k in ( dom f) holds (h /. k) = (f /. k)

        proof

          let k be Nat such that

           A4: k in ( dom f);

          ( len f) <= (( len f) + ( len g)) & k <= ( len f) by A4, FINSEQ_3: 25, NAT_1: 11;

          then

           A5: k <= ( len h) by A3, XXREAL_0: 2;

          1 <= k by A4, FINSEQ_3: 25;

          then k in ( dom h) by A5, FINSEQ_3: 25;

          

          then (h /. k) = (h . k) by PARTFUN1:def 6

          .= (f . k) by A2, A4, FINSEQ_1:def 7

          .= (f /. k) by A4, PARTFUN1:def 6;

          hence thesis;

        end;

        thus for k be Nat st k in ( dom g) holds (h /. (( len f) + k)) = (g /. k)

        proof

          let k be Nat;

          assume

           A6: k in ( dom g);

          then k <= ( len g) by FINSEQ_3: 25;

          then

           A7: (( len f) + k) <= (( len f) + ( len g)) by XREAL_1: 7;

          1 <= k by A6, FINSEQ_3: 25;

          then ( 0 + 1) <= (( len f) + k) by A1, XREAL_1: 7;

          then (( len f) + k) in ( dom h) by A3, A7, FINSEQ_3: 25;

          

          then (h /. (( len f) + k)) = (h . (( len f) + k)) by PARTFUN1:def 6

          .= (g . k) by A2, A6, FINSEQ_1:def 7

          .= (g /. k) by A6, PARTFUN1:def 6;

          hence thesis;

        end;

      end;

      assume that

       A8: ( dom h) = ( Seg (( len f) + ( len g))) and

       A9: for k be Nat st k in ( dom f) holds (h /. k) = (f /. k) and

       A10: for k be Nat st k in ( dom g) holds (h /. (( len f) + k)) = (g /. k);

      

       A11: ( len h) = (( len f) + ( len g)) by A8, FINSEQ_1:def 3;

      

       A12: for k be Nat st k in ( dom g) holds (h . (( len f) + k)) = (g . k)

      proof

        let k be Nat;

        assume

         A13: k in ( dom g);

        then k <= ( len g) by FINSEQ_3: 25;

        then

         A14: (( len f) + k) <= (( len f) + ( len g)) by XREAL_1: 7;

        1 <= k by A13, FINSEQ_3: 25;

        then ( 0 + 1) <= (( len f) + k) by A1, XREAL_1: 7;

        then (( len f) + k) in ( dom h) by A11, A14, FINSEQ_3: 25;

        

        then (h . (( len f) + k)) = (h /. (( len f) + k)) by PARTFUN1:def 6

        .= (g /. k) by A10, A13

        .= (g . k) by A13, PARTFUN1:def 6;

        hence thesis;

      end;

      for k be Nat st k in ( dom f) holds (h . k) = (f . k)

      proof

        let k be Nat such that

         A15: k in ( dom f);

        ( len f) <= (( len f) + ( len g)) & k <= ( len f) by A15, FINSEQ_3: 25, NAT_1: 11;

        then

         A16: k <= ( len h) by A11, XXREAL_0: 2;

        1 <= k by A15, FINSEQ_3: 25;

        then k in ( dom h) by A16, FINSEQ_3: 25;

        

        then (h . k) = (h /. k) by PARTFUN1:def 6

        .= (f /. k) by A9, A15

        .= (f . k) by A15, PARTFUN1:def 6;

        hence thesis;

      end;

      hence thesis by A8, A12, FINSEQ_1:def 7;

    end;

    

     Lm2: f = <*x*> iff ( len f) = 1 & (f /. 1) = x

    proof

      thus f = <*x*> implies ( len f) = 1 & (f /. 1) = x by FINSEQ_1: 40, FINSEQ_4: 16;

      assume that

       A1: ( len f) = 1 and

       A2: (f /. 1) = x;

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

      then (f . 1) = x by A2, PARTFUN1:def 6;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    

     Lm3: ((f ^ <*x*>) /. (( len f) + 1)) = x

    proof

      

       A1: 1 <= (( len f) + 1) by NAT_1: 11;

      (( len f) + 1) = (( len f) + ( len <*x*>)) by FINSEQ_1: 39

      .= ( len (f ^ <*x*>)) by FINSEQ_1: 22;

      then (( len f) + 1) in ( dom (f ^ <*x*>)) by A1, FINSEQ_3: 25;

      

      then ((f ^ <*x*>) /. (( len f) + 1)) = ((f ^ <*x*>) . (( len f) + 1)) by PARTFUN1:def 6

      .= x by FINSEQ_1: 42;

      hence thesis;

    end;

    

     Lm4: i <> 0 & i <= ( len f) implies ((f ^ g) /. i) = (f /. i)

    proof

      assume that

       A1: i <> 0 and

       A2: i <= ( len f);

       0 <= i by NAT_1: 2;

      then 0 < i by A1, XXREAL_0: 1;

      then ( 0 + 1) <= i by NAT_1: 13;

      then i in ( dom f) by A2, FINSEQ_3: 25;

      hence thesis by Lm1;

    end;

    

     Lm5: i <> 0 & i <= ( len g) implies ((f ^ g) /. (( len f) + i)) = (g /. i)

    proof

      assume that

       A1: i <> 0 and

       A2: i <= ( len g);

       0 <= i by NAT_1: 2;

      then 0 < i by A1, XXREAL_0: 1;

      then ( 0 + 1) <= i by NAT_1: 13;

      then i in ( dom g) by A2, FINSEQ_3: 25;

      hence thesis by Lm1;

    end;

    definition

      let R be non empty doubleLoopStr, x be Scalar of R;

      :: O_RING_1:def1

      func x ^2 -> Scalar of R equals (x * x);

      coherence ;

    end

    definition

      let R be non empty doubleLoopStr, x be Scalar of R;

      :: O_RING_1:def2

      attr x is being_a_square means ex y be Scalar of R st x = (y ^2 );

    end

    definition

      let R, f;

      :: O_RING_1:def3

      attr f is being_a_Sum_of_squares means ( len f) <> 0 & (f /. 1) is being_a_square & for n st n <> 0 & n < ( len f) holds ex y st y is being_a_square & (f /. (n + 1)) = ((f /. n) + y);

    end

    definition

      let R be non empty doubleLoopStr, x be Scalar of R;

      :: O_RING_1:def4

      attr x is being_a_sum_of_squares means ex f be FinSequence of R st f is being_a_Sum_of_squares & x = (f /. ( len f));

    end

    

     Lm6: x is being_a_square implies <*x*> is being_a_Sum_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_a_square & ( <*x*> /. (n + 1)) = (( <*x*> /. n) + y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_a_square;

      then

       A4: ( <*x*> /. 1) is being_a_square by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm7: x is being_a_square implies x is being_a_sum_of_squares

    proof

      assume x is being_a_square;

      then

       A1: <*x*> is being_a_Sum_of_squares by Lm6;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    definition

      let R, f;

      :: O_RING_1:def5

      attr f is being_a_Product_of_squares means ( len f) <> 0 & (f /. 1) is being_a_square & for n st n <> 0 & n < ( len f) holds ex y st y is being_a_square & (f /. (n + 1)) = ((f /. n) * y);

    end

    definition

      let R, x;

      :: O_RING_1:def6

      attr x is being_a_product_of_squares means ex f st f is being_a_Product_of_squares & x = (f /. ( len f));

    end

    

     Lm8: x is being_a_square implies <*x*> is being_a_Product_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_a_square & ( <*x*> /. (n + 1)) = (( <*x*> /. n) * y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_a_square;

      then

       A4: ( <*x*> /. 1) is being_a_square by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm9: x is being_a_square implies x is being_a_product_of_squares

    proof

      assume x is being_a_square;

      then

       A1: <*x*> is being_a_Product_of_squares by Lm8;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    definition

      let R, f;

      :: O_RING_1:def7

      attr f is being_a_Sum_of_products_of_squares means ( len f) <> 0 & (f /. 1) is being_a_product_of_squares & for n st n <> 0 & n < ( len f) holds ex y st y is being_a_product_of_squares & (f /. (n + 1)) = ((f /. n) + y);

    end

    definition

      let R, x;

      :: O_RING_1:def8

      attr x is being_a_sum_of_products_of_squares means ex f st f is being_a_Sum_of_products_of_squares & x = (f /. ( len f));

    end

    

     Lm10: x is being_a_square implies <*x*> is being_a_Sum_of_products_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_a_product_of_squares & ( <*x*> /. (n + 1)) = (( <*x*> /. n) + y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_a_square;

      then x is being_a_product_of_squares by Lm9;

      then

       A4: ( <*x*> /. 1) is being_a_product_of_squares by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm11: x is being_a_square implies x is being_a_sum_of_products_of_squares

    proof

      assume x is being_a_square;

      then

       A1: <*x*> is being_a_Sum_of_products_of_squares by Lm10;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    

     Lm12: x is being_a_product_of_squares implies <*x*> is being_a_Sum_of_products_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_a_product_of_squares & ( <*x*> /. (n + 1)) = (( <*x*> /. n) + y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_a_product_of_squares;

      then

       A4: ( <*x*> /. 1) is being_a_product_of_squares by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm13: x is being_a_product_of_squares implies x is being_a_sum_of_products_of_squares

    proof

      assume x is being_a_product_of_squares;

      then

       A1: <*x*> is being_a_Sum_of_products_of_squares by Lm12;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    

     Lm14: f is being_a_Sum_of_squares implies f is being_a_Sum_of_products_of_squares

    proof

      assume

       A1: f is being_a_Sum_of_squares;

      then (f /. 1) is being_a_square;

      then

       A2: (f /. 1) is being_a_product_of_squares by Lm9;

      

       A3: for n st n <> 0 & n < ( len f) holds ex y st y is being_a_product_of_squares & (f /. (n + 1)) = ((f /. n) + y)

      proof

        let n;

        assume n <> 0 & n < ( len f);

        then ex y st y is being_a_square & (f /. (n + 1)) = ((f /. n) + y) by A1;

        hence thesis by Lm9;

      end;

      ( len f) <> 0 by A1;

      hence thesis by A2, A3;

    end;

    

     Lm15: x is being_a_sum_of_squares implies x is being_a_sum_of_products_of_squares by Lm14;

    definition

      let R, f;

      :: O_RING_1:def9

      attr f is being_an_Amalgam_of_squares means ( len f) <> 0 & for n st n <> 0 & n <= ( len f) holds (f /. n) is being_a_product_of_squares or ex i, j st (f /. n) = ((f /. i) * (f /. j)) & i <> 0 & i < n & j <> 0 & j < n;

    end

    definition

      let R, x;

      :: O_RING_1:def10

      attr x is being_an_amalgam_of_squares means ex f st f is being_an_Amalgam_of_squares & x = (f /. ( len f));

    end

    

     Lm16: x is being_a_square implies <*x*> is being_an_Amalgam_of_squares

    proof

      assume x is being_a_square;

      then x is being_a_product_of_squares by Lm9;

      then

       A1: ( <*x*> /. 1) is being_a_product_of_squares by Lm2;

      

       A2: for n st n <> 0 & n <= ( len <*x*>) holds ( <*x*> /. n) is being_a_product_of_squares or ex i, j st ( <*x*> /. n) = (( <*x*> /. i) * ( <*x*> /. j)) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n;

        assume that

         A3: n <> 0 and

         A4: n <= ( len <*x*>);

        n <= 1 by A4, Lm2;

        hence thesis by A1, A3, NAT_1: 25;

      end;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A2;

    end;

    

     Lm17: x is being_a_square implies x is being_an_amalgam_of_squares

    proof

      assume x is being_a_square;

      then

       A1: <*x*> is being_an_Amalgam_of_squares by Lm16;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    

     Lm18: x is being_a_product_of_squares implies <*x*> is being_an_Amalgam_of_squares

    proof

      assume x is being_a_product_of_squares;

      then

       A1: ( <*x*> /. 1) is being_a_product_of_squares by Lm2;

      

       A2: for n st n <> 0 & n <= ( len <*x*>) holds ( <*x*> /. n) is being_a_product_of_squares or ex i, j st ( <*x*> /. n) = (( <*x*> /. i) * ( <*x*> /. j)) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n;

        assume that

         A3: n <> 0 and

         A4: n <= ( len <*x*>);

        n <= 1 by A4, Lm2;

        hence thesis by A1, A3, NAT_1: 25;

      end;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A2;

    end;

    

     Lm19: x is being_a_product_of_squares implies x is being_an_amalgam_of_squares

    proof

      assume x is being_a_product_of_squares;

      then

       A1: <*x*> is being_an_Amalgam_of_squares by Lm18;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    definition

      let R, f;

      :: O_RING_1:def11

      attr f is being_a_Sum_of_amalgams_of_squares means ( len f) <> 0 & (f /. 1) is being_an_amalgam_of_squares & for n st n <> 0 & n < ( len f) holds ex y st y is being_an_amalgam_of_squares & (f /. (n + 1)) = ((f /. n) + y);

    end

    definition

      let R, x;

      :: O_RING_1:def12

      attr x is being_a_sum_of_amalgams_of_squares means ex f st f is being_a_Sum_of_amalgams_of_squares & x = (f /. ( len f));

    end

    

     Lm20: x is being_a_square implies <*x*> is being_a_Sum_of_amalgams_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_an_amalgam_of_squares & ( <*x*> /. (n + 1)) = (( <*x*> /. n) + y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_a_square;

      then x is being_an_amalgam_of_squares by Lm17;

      then

       A4: ( <*x*> /. 1) is being_an_amalgam_of_squares by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm21: x is being_a_square implies x is being_a_sum_of_amalgams_of_squares

    proof

      assume x is being_a_square;

      then

       A1: <*x*> is being_a_Sum_of_amalgams_of_squares by Lm20;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    

     Lm22: f is being_a_Sum_of_squares implies f is being_a_Sum_of_amalgams_of_squares

    proof

      assume

       A1: f is being_a_Sum_of_squares;

      then (f /. 1) is being_a_square;

      then

       A2: (f /. 1) is being_an_amalgam_of_squares by Lm17;

      

       A3: for n st n <> 0 & n < ( len f) holds ex y st y is being_an_amalgam_of_squares & (f /. (n + 1)) = ((f /. n) + y)

      proof

        let n;

        assume n <> 0 & n < ( len f);

        then ex y st y is being_a_square & (f /. (n + 1)) = ((f /. n) + y) by A1;

        hence thesis by Lm17;

      end;

      ( len f) <> 0 by A1;

      hence thesis by A2, A3;

    end;

    

     Lm23: x is being_a_sum_of_squares implies x is being_a_sum_of_amalgams_of_squares by Lm22;

    

     Lm24: x is being_a_product_of_squares implies <*x*> is being_a_Sum_of_amalgams_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_an_amalgam_of_squares & ( <*x*> /. (n + 1)) = (( <*x*> /. n) + y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_a_product_of_squares;

      then x is being_an_amalgam_of_squares by Lm19;

      then

       A4: ( <*x*> /. 1) is being_an_amalgam_of_squares by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm25: x is being_a_product_of_squares implies x is being_a_sum_of_amalgams_of_squares

    proof

      assume x is being_a_product_of_squares;

      then

       A1: <*x*> is being_a_Sum_of_amalgams_of_squares by Lm24;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    

     Lm26: f is being_a_Sum_of_products_of_squares implies f is being_a_Sum_of_amalgams_of_squares

    proof

      assume

       A1: f is being_a_Sum_of_products_of_squares;

      then (f /. 1) is being_a_product_of_squares;

      then

       A2: (f /. 1) is being_an_amalgam_of_squares by Lm19;

      

       A3: for n st n <> 0 & n < ( len f) holds ex y st y is being_an_amalgam_of_squares & (f /. (n + 1)) = ((f /. n) + y)

      proof

        let n;

        assume n <> 0 & n < ( len f);

        then ex y st y is being_a_product_of_squares & (f /. (n + 1)) = ((f /. n) + y) by A1;

        hence thesis by Lm19;

      end;

      ( len f) <> 0 by A1;

      hence thesis by A2, A3;

    end;

    

     Lm27: x is being_a_sum_of_products_of_squares implies x is being_a_sum_of_amalgams_of_squares by Lm26;

    

     Lm28: x is being_an_amalgam_of_squares implies <*x*> is being_a_Sum_of_amalgams_of_squares

    proof

      

       A1: for n st n <> 0 & n < ( len <*x*>) holds ex y st y is being_an_amalgam_of_squares & ( <*x*> /. (n + 1)) = (( <*x*> /. n) + y)

      proof

        let n;

        assume that

         A2: n <> 0 and

         A3: n < ( len <*x*>);

        n < 1 by A3, Lm2;

        hence thesis by A2, NAT_1: 25;

      end;

      assume x is being_an_amalgam_of_squares;

      then

       A4: ( <*x*> /. 1) is being_an_amalgam_of_squares by Lm2;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A4, A1;

    end;

    

     Lm29: x is being_an_amalgam_of_squares implies x is being_a_sum_of_amalgams_of_squares

    proof

      assume x is being_an_amalgam_of_squares;

      then

       A1: <*x*> is being_a_Sum_of_amalgams_of_squares by Lm28;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    definition

      let R, f;

      :: O_RING_1:def13

      attr f is being_a_generation_from_squares means ( len f) <> 0 & for n st n <> 0 & n <= ( len f) holds (f /. n) is being_an_amalgam_of_squares or ex i, j st ((f /. n) = ((f /. i) * (f /. j)) or (f /. n) = ((f /. i) + (f /. j))) & i <> 0 & i < n & j <> 0 & j < n;

    end

    definition

      let R, x;

      :: O_RING_1:def14

      attr x is generated_from_squares means ex f st f is being_a_generation_from_squares & x = (f /. ( len f));

    end

    

     Lm30: x is being_a_square implies <*x*> is being_a_generation_from_squares

    proof

      assume x is being_a_square;

      then x is being_an_amalgam_of_squares by Lm17;

      then

       A1: ( <*x*> /. 1) is being_an_amalgam_of_squares by Lm2;

      

       A2: for n st n <> 0 & n <= ( len <*x*>) holds ( <*x*> /. n) is being_an_amalgam_of_squares or ex i, j st (( <*x*> /. n) = (( <*x*> /. i) * ( <*x*> /. j)) or ( <*x*> /. n) = (( <*x*> /. i) + ( <*x*> /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n;

        assume that

         A3: n <> 0 and

         A4: n <= ( len <*x*>);

        n <= 1 by A4, Lm2;

        hence thesis by A1, A3, NAT_1: 25;

      end;

      ( len <*x*>) = 1 by Lm2;

      hence thesis by A2;

    end;

    

     Lm31: x is being_a_square implies x is generated_from_squares

    proof

      assume x is being_a_square;

      then

       A1: <*x*> is being_a_generation_from_squares by Lm30;

      ( len <*x*>) = 1 & ( <*x*> /. 1) = x by Lm2;

      hence thesis by A1;

    end;

    

     Lm32: f is being_a_generation_from_squares & i <> 0 & i <= ( len f) & j <> 0 & j <= ( len f) implies (f ^ <*((f /. i) + (f /. j))*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: i <> 0 and

       A3: i <= ( len f) and

       A4: j <> 0 and

       A5: j <= ( len f);

      set g = (f ^ <*((f /. i) + (f /. j))*>);

      

       A6: ( len g) = (( len f) + ( len <*((f /. i) + (f /. j))*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A7: for n st n <> 0 & n <= ( len g) holds (g /. n) is being_an_amalgam_of_squares or ex i, j st ((g /. n) = ((g /. i) * (g /. j)) or (g /. n) = ((g /. i) + (g /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A8: n <> 0 and

         A9: n <= ( len g);

         A10:

        now

          assume n < ( len g);

          then

           A11: n <= ( len f) by A6, NAT_1: 13;

          then

           A12: (g /. n) = (f /. n) by A8, Lm4;

           A13:

          now

            given k, m such that

             A14: (f /. n) = ((f /. k) * (f /. m)) or (f /. n) = ((f /. k) + (f /. m)) and

             A15: k <> 0 & k < n & m <> 0 & m < n;

            (f /. k) = (g /. k) & (f /. m) = (g /. m) by A11, A15, Lm4, XXREAL_0: 2;

            hence thesis by A12, A14, A15;

          end;

          (f /. n) is being_an_amalgam_of_squares implies thesis by A8, A11, Lm4;

          hence thesis by A1, A8, A11, A13;

        end;

        now

          assume

           A16: n = ( len g);

          then

           A17: i < n & j < n by A3, A5, A6, NAT_1: 13;

          (g /. n) = ((f /. i) + (f /. j)) by A6, A16, Lm3

          .= ((g /. i) + (f /. j)) by A2, A3, Lm4

          .= ((g /. i) + (g /. j)) by A4, A5, Lm4;

          hence thesis by A2, A4, A17;

        end;

        hence thesis by A9, A10, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len <*((f /. i) + (f /. j))*>)) <> 0 ;

      then ( len (f ^ <*((f /. i) + (f /. j))*>)) <> 0 by FINSEQ_1: 22;

      hence thesis by A7;

    end;

    

     Lm33: f is being_a_generation_from_squares & g is being_a_generation_from_squares implies (f ^ g) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: g is being_a_generation_from_squares;

      

       A3: for n st n <> 0 & n <= ( len (f ^ g)) holds ((f ^ g) /. n) is being_an_amalgam_of_squares or ex i, j st (((f ^ g) /. n) = (((f ^ g) /. i) * ((f ^ g) /. j)) or ((f ^ g) /. n) = (((f ^ g) /. i) + ((f ^ g) /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n;

        assume that

         A4: n <> 0 and

         A5: n <= ( len (f ^ g));

        

         A6: n <= (( len f) + ( len g)) by A5, FINSEQ_1: 22;

         A7:

        now

          assume

           A8: ( len f) < n;

          then

          consider m be Nat such that

           A9: n = (( len f) + m) by NAT_1: 10;

          (( len f) + m) <= (( len f) + ( len g)) by A5, A9, FINSEQ_1: 22;

          then

           A10: m <= ( len g) by XREAL_1: 6;

          

           A11: m <> 0 by A8, A9;

          

           A12: m <= ( len g) by A6, A9, XREAL_1: 6;

           A13:

          now

            given k,l be Nat such that

             A14: (g /. m) = ((g /. k) * (g /. l)) or (g /. m) = ((g /. k) + (g /. l)) and

             A15: k <> 0 and

             A16: k < m and

             A17: l <> 0 and

             A18: l < m;

            

             A19: (( len f) + k) <> 0 & (( len f) + l) <> 0 by A15, A17;

            

             A20: ((f ^ g) /. n) = (((f ^ g) /. (( len f) + k)) * ((f ^ g) /. (( len f) + l))) or ((f ^ g) /. n) = (((f ^ g) /. (( len f) + k)) + ((f ^ g) /. (( len f) + l)))

            proof

               A21:

              now

                assume (g /. m) = ((g /. k) + (g /. l));

                

                then ((f ^ g) /. n) = ((g /. k) + (g /. l)) by A9, A11, A10, Lm5

                .= (((f ^ g) /. (( len f) + k)) + (g /. l)) by A12, A15, A16, Lm5, XXREAL_0: 2

                .= (((f ^ g) /. (( len f) + k)) + ((f ^ g) /. (( len f) + l))) by A12, A17, A18, Lm5, XXREAL_0: 2;

                hence thesis;

              end;

              now

                assume (g /. m) = ((g /. k) * (g /. l));

                

                then ((f ^ g) /. n) = ((g /. k) * (g /. l)) by A9, A11, A10, Lm5

                .= (((f ^ g) /. (( len f) + k)) * (g /. l)) by A12, A15, A16, Lm5, XXREAL_0: 2

                .= (((f ^ g) /. (( len f) + k)) * ((f ^ g) /. (( len f) + l))) by A12, A17, A18, Lm5, XXREAL_0: 2;

                hence thesis;

              end;

              hence thesis by A14, A21;

            end;

            (( len f) + k) < n & (( len f) + l) < n by A9, A16, A18, XREAL_1: 6;

            hence thesis by A20, A19;

          end;

          (g /. m) is being_an_amalgam_of_squares implies thesis by A9, A11, A10, Lm5;

          hence thesis by A2, A11, A10, A13;

        end;

        now

          assume

           A22: n <= ( len f);

          then

           A23: ((f ^ g) /. n) = (f /. n) by A4, Lm4;

           A24:

          now

            given k,l be Nat such that

             A25: (f /. n) = ((f /. k) * (f /. l)) or (f /. n) = ((f /. k) + (f /. l)) and

             A26: k <> 0 & k < n & l <> 0 & l < n;

            ((f ^ g) /. k) = (f /. k) & ((f ^ g) /. l) = (f /. l) by A22, A26, Lm4, XXREAL_0: 2;

            hence thesis by A23, A25, A26;

          end;

          (f /. n) is being_an_amalgam_of_squares implies thesis by A4, A22, Lm4;

          hence thesis by A1, A4, A22, A24;

        end;

        hence thesis by A7;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len g)) <> 0 ;

      then ( len (f ^ g)) <> 0 by FINSEQ_1: 22;

      hence thesis by A3;

    end;

    

     Lm34: f is being_a_generation_from_squares & x is being_a_square implies (f ^ <*x*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: x is being_a_square;

       <*x*> is being_a_generation_from_squares by A2, Lm30;

      hence thesis by A1, Lm33;

    end;

    

     Lm35: f is being_a_generation_from_squares & x is being_a_square implies ((f ^ <*x*>) ^ <*((f /. ( len f)) + x)*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: x is being_a_square;

      

       A3: (f ^ <*x*>) is being_a_generation_from_squares by A1, A2, Lm34;

      ( len <*x*>) = 1 by Lm2;

      then

       A4: (( len f) + 1) = ( len (f ^ <*x*>)) by FINSEQ_1: 22;

      

       A5: ( len f) <= (( len f) + 1) & (( len f) + 1) <> 0 by NAT_1: 11;

      

       A6: ((f ^ <*x*>) /. (( len f) + 1)) = x by Lm3;

      

       A7: ( len f) <> 0 by A1;

      then ((f ^ <*x*>) /. ( len f)) = (f /. ( len f)) by Lm4;

      hence thesis by A3, A7, A5, A4, A6, Lm32;

    end;

    

     Lm36: x is generated_from_squares & y is being_a_square implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_square;

      consider f such that

       A3: f is being_a_generation_from_squares & x = (f /. ( len f)) by A1;

      take g = ((f ^ <*y*>) ^ <*((f /. ( len f)) + y)*>);

      ( len g) = (( len (f ^ <*y*>)) + ( len <*((f /. ( len f)) + y)*>)) by FINSEQ_1: 22

      .= (( len (f ^ <*y*>)) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm35;

    end;

    

     Lm37: f is being_a_Sum_of_squares & 0 <> i & i <= ( len f) implies (f /. i) is generated_from_squares

    proof

      assume that

       A1: f is being_a_Sum_of_squares and

       A2: 0 <> i & i <= ( len f);

      defpred P[ Nat] means 0 <> $1 & $1 <= ( len f) implies (f /. $1) is generated_from_squares;

      

       A3: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A4: 0 <> i & i <= ( len f) implies (f /. i) is generated_from_squares;

        assume that 0 <> (i + 1) and

         A5: (i + 1) <= ( len f);

        

         A6: i < ( len f) by A5, NAT_1: 13;

         A7:

        now

          assume

           A8: i <> 0 ;

          then ex y st y is being_a_square & (f /. (i + 1)) = ((f /. i) + y) by A1, A6;

          hence thesis by A4, A5, A8, Lm36, NAT_1: 13;

        end;

        i = 0 implies thesis by A1, Lm31;

        hence thesis by A7;

      end;

      

       A9: P[ 0 ];

      for i holds P[i] from NAT_1:sch 2( A9, A3);

      hence thesis by A2;

    end;

    

     Lm38: x is being_a_sum_of_squares implies x is generated_from_squares

    proof

      assume x is being_a_sum_of_squares;

      then

      consider f such that

       A1: f is being_a_Sum_of_squares and

       A2: x = (f /. ( len f));

      thus thesis by A1, A2, Lm37;

    end;

    

     Lm39: f is being_an_Amalgam_of_squares implies f is being_a_generation_from_squares

    proof

      assume

       A1: f is being_an_Amalgam_of_squares;

      hence ( len f) <> 0 ;

      let n such that

       A2: n <> 0 & n <= ( len f);

      

       A3: (ex i, j st (f /. n) = ((f /. i) * (f /. j)) & i <> 0 & i < n & j <> 0 & j < n) implies thesis;

      (f /. n) is being_a_product_of_squares implies thesis by Lm19;

      hence thesis by A1, A2, A3;

    end;

    

     Lm40: x is being_an_amalgam_of_squares implies x is generated_from_squares by Lm39;

    

     Lm41: x is being_an_amalgam_of_squares implies <*x*> is being_a_generation_from_squares

    proof

      set g = <*x*>;

      assume

       A1: x is being_an_amalgam_of_squares;

      

       A2: for n st n <> 0 & n <= ( len g) holds (g /. n) is being_an_amalgam_of_squares or ex i, j st ((g /. n) = ((g /. i) * (g /. j)) or (g /. n) = ((g /. i) + (g /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A3: n <> 0 and

         A4: n <= ( len g);

        n <= 1 by A4, Lm2;

        then n < (1 + 1) by NAT_1: 13;

        then n = 1 by A3, NAT_1: 23;

        hence thesis by A1, Lm2;

      end;

      ( len g) = 1 by Lm2;

      hence thesis by A2;

    end;

    

     Lm42: f is being_a_generation_from_squares & x is being_an_amalgam_of_squares implies ((f ^ <*x*>) ^ <*((f /. ( len f)) + x)*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: x is being_an_amalgam_of_squares;

       <*x*> is being_a_generation_from_squares by A2, Lm41;

      then

       A3: (f ^ <*x*>) is being_a_generation_from_squares by A1, Lm33;

      ( len <*x*>) = 1 by Lm2;

      then

       A4: (( len f) + 1) = ( len (f ^ <*x*>)) by FINSEQ_1: 22;

      

       A5: ( len f) <= (( len f) + 1) & (( len f) + 1) <> 0 by NAT_1: 11;

      

       A6: ((f ^ <*x*>) /. (( len f) + 1)) = x by Lm3;

      

       A7: ( len f) <> 0 by A1;

      then ((f ^ <*x*>) /. ( len f)) = (f /. ( len f)) by Lm4;

      hence thesis by A3, A7, A5, A4, A6, Lm32;

    end;

    

     Lm43: x is generated_from_squares & y is being_an_amalgam_of_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_an_amalgam_of_squares;

      consider f such that

       A3: f is being_a_generation_from_squares & x = (f /. ( len f)) by A1;

      take g = ((f ^ <*y*>) ^ <*((f /. ( len f)) + y)*>);

      ( len g) = (( len (f ^ <*y*>)) + ( len <*((f /. ( len f)) + y)*>)) by FINSEQ_1: 22

      .= (( len (f ^ <*y*>)) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm42;

    end;

    

     Lm44: f is being_a_Sum_of_amalgams_of_squares implies for i holds i <> 0 & i <= ( len f) implies (f /. i) is generated_from_squares

    proof

      defpred P[ Nat] means $1 <> 0 & $1 <= ( len f) implies (f /. $1) is generated_from_squares;

      assume

       A1: f is being_a_Sum_of_amalgams_of_squares;

      

       A2: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A3: i <> 0 & i <= ( len f) implies (f /. i) is generated_from_squares;

        assume that (i + 1) <> 0 and

         A4: (i + 1) <= ( len f);

         A5:

        now

          assume

           A6: i <> 0 ;

          i < ( len f) by A4, NAT_1: 13;

          then ex y st y is being_an_amalgam_of_squares & (f /. (i + 1)) = ((f /. i) + y) by A1, A6;

          hence thesis by A3, A4, A6, Lm43, NAT_1: 13;

        end;

        i = 0 implies thesis by A1, Lm40;

        hence thesis by A5;

      end;

      

       A7: P[ 0 ];

      thus for i holds P[i] from NAT_1:sch 2( A7, A2);

    end;

    theorem :: O_RING_1:1

    

     Th1: x is being_a_sum_of_amalgams_of_squares implies x is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares;

      then

      consider f such that

       A1: f is being_a_Sum_of_amalgams_of_squares and

       A2: x = (f /. ( len f));

      thus thesis by A1, A2, Lm44;

    end;

    

     Lm45: f is being_a_generation_from_squares & i <> 0 & i <= ( len f) & j <> 0 & j <= ( len f) implies (f ^ <*((f /. i) * (f /. j))*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: i <> 0 and

       A3: i <= ( len f) and

       A4: j <> 0 and

       A5: j <= ( len f);

      set g = (f ^ <*((f /. i) * (f /. j))*>);

      

       A6: ( len g) = (( len f) + ( len <*((f /. i) * (f /. j))*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A7: for n st n <> 0 & n <= ( len g) holds (g /. n) is being_an_amalgam_of_squares or ex i, j st ((g /. n) = ((g /. i) * (g /. j)) or (g /. n) = ((g /. i) + (g /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A8: n <> 0 and

         A9: n <= ( len g);

         A10:

        now

          assume n < ( len g);

          then

           A11: n <= ( len f) by A6, NAT_1: 13;

          then

           A12: (g /. n) = (f /. n) by A8, Lm4;

           A13:

          now

            given k, m such that

             A14: (f /. n) = ((f /. k) * (f /. m)) or (f /. n) = ((f /. k) + (f /. m)) and

             A15: k <> 0 & k < n & m <> 0 & m < n;

            (f /. k) = (g /. k) & (f /. m) = (g /. m) by A11, A15, Lm4, XXREAL_0: 2;

            hence thesis by A12, A14, A15;

          end;

          (f /. n) is being_an_amalgam_of_squares implies thesis by A8, A11, Lm4;

          hence thesis by A1, A8, A11, A13;

        end;

        now

          assume

           A16: n = ( len g);

          then

           A17: i < n & j < n by A3, A5, A6, NAT_1: 13;

          (g /. n) = ((f /. i) * (f /. j)) by A6, A16, Lm3

          .= ((g /. i) * (f /. j)) by A2, A3, Lm4

          .= ((g /. i) * (g /. j)) by A4, A5, Lm4;

          hence thesis by A2, A4, A17;

        end;

        hence thesis by A9, A10, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len <*((f /. i) * (f /. j))*>)) <> 0 ;

      then ( len (f ^ <*((f /. i) * (f /. j))*>)) <> 0 by FINSEQ_1: 22;

      hence thesis by A7;

    end;

    

     Lm46: f is being_a_generation_from_squares & x is being_a_square implies ((f ^ <*x*>) ^ <*((f /. ( len f)) * x)*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: x is being_a_square;

      

       A3: (f ^ <*x*>) is being_a_generation_from_squares by A1, A2, Lm34;

      ( len <*x*>) = 1 by Lm2;

      then

       A4: (( len f) + 1) = ( len (f ^ <*x*>)) by FINSEQ_1: 22;

      

       A5: ( len f) <= (( len f) + 1) & (( len f) + 1) <> 0 by NAT_1: 11;

      

       A6: ((f ^ <*x*>) /. (( len f) + 1)) = x by Lm3;

      

       A7: ( len f) <> 0 by A1;

      then ((f ^ <*x*>) /. ( len f)) = (f /. ( len f)) by Lm4;

      hence thesis by A3, A7, A5, A4, A6, Lm45;

    end;

    

     Lm47: x is generated_from_squares & y is being_a_square implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_square;

      consider f such that

       A3: f is being_a_generation_from_squares & x = (f /. ( len f)) by A1;

      take g = ((f ^ <*y*>) ^ <*((f /. ( len f)) * y)*>);

      ( len g) = (( len (f ^ <*y*>)) + ( len <*((f /. ( len f)) * y)*>)) by FINSEQ_1: 22

      .= (( len (f ^ <*y*>)) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm46;

    end;

    

     Lm48: f is being_a_Product_of_squares & 0 <> i & i <= ( len f) implies (f /. i) is generated_from_squares

    proof

      assume that

       A1: f is being_a_Product_of_squares and

       A2: 0 <> i & i <= ( len f);

      defpred P[ Nat] means 0 <> $1 & $1 <= ( len f) implies (f /. $1) is generated_from_squares;

      

       A3: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A4: 0 <> i & i <= ( len f) implies (f /. i) is generated_from_squares;

        assume that 0 <> (i + 1) and

         A5: (i + 1) <= ( len f);

        

         A6: i < ( len f) by A5, NAT_1: 13;

         A7:

        now

          assume

           A8: i <> 0 ;

          then ex y st y is being_a_square & (f /. (i + 1)) = ((f /. i) * y) by A1, A6;

          hence thesis by A4, A5, A8, Lm47, NAT_1: 13;

        end;

        i = 0 implies thesis by A1, Lm31;

        hence thesis by A7;

      end;

      

       A9: P[ 0 ];

      for i holds P[i] from NAT_1:sch 2( A9, A3);

      hence thesis by A2;

    end;

    

     Lm49: x is being_a_product_of_squares implies x is generated_from_squares

    proof

      assume x is being_a_product_of_squares;

      then

      consider f such that

       A1: f is being_a_Product_of_squares and

       A2: x = (f /. ( len f));

      thus thesis by A1, A2, Lm48;

    end;

    

     Lm50: x is being_a_product_of_squares implies <*x*> is being_a_generation_from_squares

    proof

      set g = <*x*>;

      

       A1: ( len g) = 1 by Lm2;

      assume

       A2: x is being_a_product_of_squares;

      for n st n <> 0 & n <= ( len g) holds (g /. n) is being_an_amalgam_of_squares or ex i, j st ((g /. n) = ((g /. i) * (g /. j)) or (g /. n) = ((g /. i) + (g /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A3: n <> 0 and

         A4: n <= ( len g);

        n < (1 + 1) by A1, A4, NAT_1: 13;

        then n = 1 by A3, NAT_1: 23;

        then (g /. n) = x by Lm2;

        hence thesis by A2, Lm19;

      end;

      hence thesis by A1;

    end;

    

     Lm51: f is being_a_generation_from_squares & x is being_a_product_of_squares implies ((f ^ <*x*>) ^ <*((f /. ( len f)) + x)*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: x is being_a_product_of_squares;

       <*x*> is being_a_generation_from_squares by A2, Lm50;

      then

       A3: (f ^ <*x*>) is being_a_generation_from_squares by A1, Lm33;

      ( len <*x*>) = 1 by Lm2;

      then

       A4: (( len f) + 1) = ( len (f ^ <*x*>)) by FINSEQ_1: 22;

      

       A5: ( len f) <= (( len f) + 1) & (( len f) + 1) <> 0 by NAT_1: 11;

      

       A6: ((f ^ <*x*>) /. (( len f) + 1)) = x by Lm3;

      

       A7: ( len f) <> 0 by A1;

      then ((f ^ <*x*>) /. ( len f)) = (f /. ( len f)) by Lm4;

      hence thesis by A3, A7, A5, A4, A6, Lm32;

    end;

    

     Lm52: x is generated_from_squares & y is being_a_product_of_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_product_of_squares;

      consider f such that

       A3: f is being_a_generation_from_squares & x = (f /. ( len f)) by A1;

      take g = ((f ^ <*y*>) ^ <*((f /. ( len f)) + y)*>);

      ( len g) = (( len (f ^ <*y*>)) + ( len <*((f /. ( len f)) + y)*>)) by FINSEQ_1: 22

      .= (( len (f ^ <*y*>)) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm51;

    end;

    

     Lm53: f is being_a_Sum_of_products_of_squares & 0 <> i & i <= ( len f) implies (f /. i) is generated_from_squares

    proof

      assume that

       A1: f is being_a_Sum_of_products_of_squares and

       A2: 0 <> i & i <= ( len f);

      defpred P[ Nat] means 0 <> $1 & $1 <= ( len f) implies (f /. $1) is generated_from_squares;

      

       A3: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A4: 0 <> i & i <= ( len f) implies (f /. i) is generated_from_squares;

        assume that 0 <> (i + 1) and

         A5: (i + 1) <= ( len f);

        

         A6: i < ( len f) by A5, NAT_1: 13;

         A7:

        now

          assume

           A8: i <> 0 ;

          then ex y st y is being_a_product_of_squares & (f /. (i + 1)) = ((f /. i) + y) by A1, A6;

          hence thesis by A4, A5, A8, Lm52, NAT_1: 13;

        end;

        i = 0 implies thesis by A1, Lm49;

        hence thesis by A7;

      end;

      

       A9: P[ 0 ];

      for i holds P[i] from NAT_1:sch 2( A9, A3);

      hence thesis by A2;

    end;

    

     Lm54: x is being_a_sum_of_products_of_squares implies x is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares;

      then

      consider f such that

       A1: f is being_a_Sum_of_products_of_squares and

       A2: x = (f /. ( len f));

      thus thesis by A1, A2, Lm53;

    end;

    theorem :: O_RING_1:2

    x is being_a_square implies x is being_a_sum_of_squares & x is being_a_product_of_squares & x is being_a_sum_of_products_of_squares & x is being_an_amalgam_of_squares & x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm7, Lm9, Lm11, Lm17, Lm21, Lm31;

    theorem :: O_RING_1:3

    x is being_a_sum_of_squares implies x is being_a_sum_of_products_of_squares & x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm15, Lm23, Lm38;

    theorem :: O_RING_1:4

    x is being_a_product_of_squares implies x is being_a_sum_of_products_of_squares & x is being_an_amalgam_of_squares & x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm13, Lm19, Lm25, Lm49;

    theorem :: O_RING_1:5

    x is being_a_sum_of_products_of_squares implies x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm27, Lm54;

    theorem :: O_RING_1:6

    x is being_an_amalgam_of_squares implies x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm29, Lm40;

    begin

    

     Lm55: f is being_a_Sum_of_squares & x is being_a_square implies (f ^ <*((f /. ( len f)) + x)*>) is being_a_Sum_of_squares

    proof

      assume that

       A1: f is being_a_Sum_of_squares and

       A2: x is being_a_square;

      set g = (f ^ <*((f /. ( len f)) + x)*>);

      

       A3: ( len g) = (( len f) + ( len <*((f /. ( len f)) + x)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A4: for n st n <> 0 & n < ( len g) holds (f /. n) = (g /. n)

      proof

        let n;

        assume n <> 0 & n < ( len g);

        then 1 <= n & n <= ( len f) by A3, NAT_1: 13, NAT_1: 25;

        then n in ( dom f) by FINSEQ_3: 25;

        hence thesis by Lm1;

      end;

      

       A5: for n st n <> 0 & n < ( len g) holds ex y st y is being_a_square & (g /. (n + 1)) = ((g /. n) + y)

      proof

        let n;

        assume that

         A6: n <> 0 and

         A7: n < ( len g);

         A8:

        now

          

           A9: (f /. n) = (g /. n) by A4, A6, A7;

          assume

           A10: n < ( len f);

          then (n + 1) <> 0 & (n + 1) < ( len g) by A3, XREAL_1: 6;

          then (f /. (n + 1)) = (g /. (n + 1)) by A4;

          hence thesis by A1, A6, A10, A9;

        end;

         A11:

        now

          assume

           A12: n = ( len f);

          1 <= n by A6, NAT_1: 25;

          then

           A13: n in ( dom f) by A12, FINSEQ_3: 25;

          (g /. (n + 1)) = ((f /. n) + x) by A12, Lm3;

          then (g /. (n + 1)) = ((g /. n) + x) by A13, Lm1;

          hence thesis by A2;

        end;

        n <= ( len f) by A3, A7, NAT_1: 13;

        hence thesis by A8, A11, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then 1 <= ( len f) by NAT_1: 25;

      then 1 < ( len g) by A3, NAT_1: 13;

      then (g /. 1) = (f /. 1) by A4;

      then

       A14: (g /. 1) is being_a_square by A1;

      ( len g) <> 0 by A3;

      hence thesis by A14, A5;

    end;

    

     Lm56: x is being_a_sum_of_squares & y is being_a_square implies (x + y) is being_a_sum_of_squares

    proof

      assume that

       A1: x is being_a_sum_of_squares and

       A2: y is being_a_square;

      consider f such that

       A3: f is being_a_Sum_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm55;

    end;

    

     Lm57: f is being_a_Sum_of_products_of_squares & x is being_a_product_of_squares implies (f ^ <*((f /. ( len f)) + x)*>) is being_a_Sum_of_products_of_squares

    proof

      assume that

       A1: f is being_a_Sum_of_products_of_squares and

       A2: x is being_a_product_of_squares;

      set g = (f ^ <*((f /. ( len f)) + x)*>);

      

       A3: ( len g) = (( len f) + ( len <*((f /. ( len f)) + x)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A4: for n st n <> 0 & n < ( len g) holds (f /. n) = (g /. n)

      proof

        let n;

        assume n <> 0 & n < ( len g);

        then 1 <= n & n <= ( len f) by A3, NAT_1: 13, NAT_1: 25;

        then n in ( dom f) by FINSEQ_3: 25;

        hence thesis by Lm1;

      end;

      

       A5: for n st n <> 0 & n < ( len g) holds ex y st y is being_a_product_of_squares & (g /. (n + 1)) = ((g /. n) + y)

      proof

        let n;

        assume that

         A6: n <> 0 and

         A7: n < ( len g);

         A8:

        now

          

           A9: (f /. n) = (g /. n) by A4, A6, A7;

          assume

           A10: n < ( len f);

          then (n + 1) <> 0 & (n + 1) < ( len g) by A3, XREAL_1: 6;

          then (f /. (n + 1)) = (g /. (n + 1)) by A4;

          hence thesis by A1, A6, A10, A9;

        end;

         A11:

        now

          assume

           A12: n = ( len f);

          1 <= n by A6, NAT_1: 25;

          then

           A13: n in ( dom f) by A12, FINSEQ_3: 25;

          (g /. (n + 1)) = ((f /. n) + x) by A12, Lm3;

          then (g /. (n + 1)) = ((g /. n) + x) by A13, Lm1;

          hence thesis by A2;

        end;

        n <= ( len f) by A3, A7, NAT_1: 13;

        hence thesis by A8, A11, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then 1 <= ( len f) by NAT_1: 25;

      then 1 < ( len g) by A3, NAT_1: 13;

      then (g /. 1) = (f /. 1) by A4;

      then

       A14: (g /. 1) is being_a_product_of_squares by A1;

      ( len g) <> 0 by A3;

      hence thesis by A14, A5;

    end;

    

     Lm58: x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares implies (x + y) is being_a_sum_of_products_of_squares

    proof

      assume that

       A1: x is being_a_sum_of_products_of_squares and

       A2: y is being_a_product_of_squares;

      consider f such that

       A3: f is being_a_Sum_of_products_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm57;

    end;

    

     Lm59: f is being_a_Sum_of_amalgams_of_squares & x is being_an_amalgam_of_squares implies (f ^ <*((f /. ( len f)) + x)*>) is being_a_Sum_of_amalgams_of_squares

    proof

      assume that

       A1: f is being_a_Sum_of_amalgams_of_squares and

       A2: x is being_an_amalgam_of_squares;

      set g = (f ^ <*((f /. ( len f)) + x)*>);

      

       A3: ( len g) = (( len f) + ( len <*((f /. ( len f)) + x)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A4: for n st n <> 0 & n < ( len g) holds (f /. n) = (g /. n)

      proof

        let n;

        assume n <> 0 & n < ( len g);

        then 1 <= n & n <= ( len f) by A3, NAT_1: 13, NAT_1: 25;

        then n in ( dom f) by FINSEQ_3: 25;

        hence thesis by Lm1;

      end;

      

       A5: for n st n <> 0 & n < ( len g) holds ex y st y is being_an_amalgam_of_squares & (g /. (n + 1)) = ((g /. n) + y)

      proof

        let n;

        assume that

         A6: n <> 0 and

         A7: n < ( len g);

         A8:

        now

          

           A9: (f /. n) = (g /. n) by A4, A6, A7;

          assume

           A10: n < ( len f);

          then (n + 1) <> 0 & (n + 1) < ( len g) by A3, XREAL_1: 6;

          then (f /. (n + 1)) = (g /. (n + 1)) by A4;

          hence thesis by A1, A6, A10, A9;

        end;

         A11:

        now

          assume

           A12: n = ( len f);

          1 <= n by A6, NAT_1: 25;

          then

           A13: n in ( dom f) by A12, FINSEQ_3: 25;

          (g /. (n + 1)) = ((f /. n) + x) by A12, Lm3;

          then (g /. (n + 1)) = ((g /. n) + x) by A13, Lm1;

          hence thesis by A2;

        end;

        n <= ( len f) by A3, A7, NAT_1: 13;

        hence thesis by A8, A11, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then 1 <= ( len f) by NAT_1: 25;

      then 1 < ( len g) by A3, NAT_1: 13;

      then (g /. 1) = (f /. 1) by A4;

      then

       A14: (g /. 1) is being_an_amalgam_of_squares by A1;

      ( len g) <> 0 by A3;

      hence thesis by A14, A5;

    end;

    

     Lm60: x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares implies (x + y) is being_a_sum_of_amalgams_of_squares

    proof

      assume that

       A1: x is being_a_sum_of_amalgams_of_squares and

       A2: y is being_an_amalgam_of_squares;

      consider f such that

       A3: f is being_a_Sum_of_amalgams_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm59;

    end;

    

     Lm61: f is being_a_generation_from_squares & i <> 0 & i <= ( len f) & j <> 0 & j <= ( len f) implies (f ^ <*((f /. i) + (f /. j))*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: i <> 0 and

       A3: i <= ( len f) and

       A4: j <> 0 and

       A5: j <= ( len f);

      set g = (f ^ <*((f /. i) + (f /. j))*>);

      

       A6: ( len g) = (( len f) + ( len <*((f /. i) + (f /. j))*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A7: for n st n <> 0 & n <= ( len g) holds (g /. n) is being_an_amalgam_of_squares or ex i, j st ((g /. n) = ((g /. i) * (g /. j)) or (g /. n) = ((g /. i) + (g /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A8: n <> 0 and

         A9: n <= ( len g);

         A10:

        now

          assume n < ( len g);

          then

           A11: n <= ( len f) by A6, NAT_1: 13;

          then

           A12: (g /. n) = (f /. n) by A8, Lm4;

           A13:

          now

            given k, m such that

             A14: (f /. n) = ((f /. k) * (f /. m)) or (f /. n) = ((f /. k) + (f /. m)) and

             A15: k <> 0 & k < n & m <> 0 & m < n;

            (f /. k) = (g /. k) & (f /. m) = (g /. m) by A11, A15, Lm4, XXREAL_0: 2;

            hence thesis by A12, A14, A15;

          end;

          (f /. n) is being_an_amalgam_of_squares implies thesis by A8, A11, Lm4;

          hence thesis by A1, A8, A11, A13;

        end;

        now

          assume

           A16: n = ( len g);

          then

           A17: i < n & j < n by A3, A5, A6, NAT_1: 13;

          (g /. n) = ((f /. i) + (f /. j)) by A6, A16, Lm3

          .= ((g /. i) + (f /. j)) by A2, A3, Lm4

          .= ((g /. i) + (g /. j)) by A4, A5, Lm4;

          hence thesis by A2, A4, A17;

        end;

        hence thesis by A9, A10, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len <*((f /. i) + (f /. j))*>)) <> 0 ;

      then ( len (f ^ <*((f /. i) + (f /. j))*>)) <> 0 by FINSEQ_1: 22;

      hence thesis by A7;

    end;

    

     Lm62: x is being_a_square & y is being_a_square implies (x + y) is being_a_sum_of_squares

    proof

      assume

       A1: x is being_a_square & y is being_a_square;

      take g = ( <*x*> ^ <*(x + y)*>);

      ( len <*x*>) = 1 by Lm2;

      then

       A2: ( <*x*> /. ( len <*x*>)) = x by Lm2;

      ( len g) = (( len <*x*>) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len <*x*>) + 1) by Lm2;

      hence thesis by A1, A2, Lm3, Lm6, Lm55;

    end;

    

     Lm63: f is being_a_generation_from_squares & g is being_a_generation_from_squares implies ((f ^ g) ^ <*((f /. ( len f)) + (g /. ( len g)))*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: g is being_a_generation_from_squares;

      

       A3: ( len g) <> 0 by A2;

      ( len f) <> 0 by A1;

      then 1 <= ( len f) by NAT_1: 25;

      then ( len f) in ( dom f) by FINSEQ_3: 25;

      then

       A4: (( len f) + ( len g)) <= ( len (f ^ g)) & ((f ^ g) /. ( len f)) = (f /. ( len f)) by Lm1, FINSEQ_1: 22;

      ( len f) <= (( len f) + ( len g)) by NAT_1: 11;

      then

       A5: ( len f) <= ( len (f ^ g)) by FINSEQ_1: 22;

      1 <= ( len g) by A3, NAT_1: 25;

      then ( len g) in ( dom g) by FINSEQ_3: 25;

      then

       A6: ((f ^ g) /. (( len f) + ( len g))) = (g /. ( len g)) by Lm1;

      (f ^ g) is being_a_generation_from_squares & ( len f) <> 0 by A1, A2, Lm33;

      hence thesis by A5, A4, A6, Lm61;

    end;

    

     Lm64: x is generated_from_squares & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is generated_from_squares;

      consider f such that

       A3: f is being_a_generation_from_squares and

       A4: x = (f /. ( len f)) by A1;

      consider g such that

       A5: g is being_a_generation_from_squares and

       A6: y = (g /. ( len g)) by A2;

      set h = ((f ^ g) ^ <*((f /. ( len f)) + (g /. ( len g)))*>);

      ( len h) = (( len (f ^ g)) + ( len <*((f /. ( len f)) + (g /. ( len g)))*>)) by FINSEQ_1: 22

      .= (( len (f ^ g)) + 1) by Lm2;

      then

       A7: (h /. ( len h)) = (x + (g /. ( len g))) by A4, Lm3;

      h is being_a_generation_from_squares by A3, A5, Lm63;

      hence thesis by A6, A7;

    end;

    theorem :: O_RING_1:7

    x is being_a_square & y is being_a_square or x is being_a_sum_of_squares & y is being_a_square implies (x + y) is being_a_sum_of_squares by Lm56, Lm62;

    

     Lm65: x is being_a_sum_of_products_of_squares & y is being_a_square implies (x + y) is being_a_sum_of_products_of_squares

    proof

      assume that

       A1: x is being_a_sum_of_products_of_squares and

       A2: y is being_a_square;

      consider f such that

       A3: f is being_a_Sum_of_products_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm9, Lm57;

    end;

    theorem :: O_RING_1:8

    x is being_a_sum_of_products_of_squares & y is being_a_square or x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares implies (x + y) is being_a_sum_of_products_of_squares by Lm58, Lm65;

    

     Lm66: x is being_an_amalgam_of_squares & y is being_a_product_of_squares implies (x + y) is being_a_sum_of_amalgams_of_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is being_a_product_of_squares;

      x is being_a_sum_of_amalgams_of_squares by A1, Lm29;

      then

      consider f such that

       A3: f is being_a_Sum_of_amalgams_of_squares & x = (f /. ( len f));

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm19, Lm59;

    end;

    

     Lm67: x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares implies (x + y) is being_a_sum_of_amalgams_of_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is being_an_amalgam_of_squares;

      x is being_a_sum_of_amalgams_of_squares by A1, Lm29;

      then

      consider f such that

       A3: f is being_a_Sum_of_amalgams_of_squares & x = (f /. ( len f));

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm59;

    end;

    

     Lm68: x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares implies (x + y) is being_a_sum_of_amalgams_of_squares

    proof

      assume that

       A1: x is being_a_sum_of_amalgams_of_squares and

       A2: y is being_a_product_of_squares;

      consider f such that

       A3: f is being_a_Sum_of_amalgams_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm19, Lm59;

    end;

    

     Lm69: x is being_a_sum_of_amalgams_of_squares & y is being_a_square implies (x + y) is being_a_sum_of_amalgams_of_squares

    proof

      assume that

       A1: x is being_a_sum_of_amalgams_of_squares and

       A2: y is being_a_square;

      consider f such that

       A3: f is being_a_Sum_of_amalgams_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x + y)*>);

      ( len g) = (( len f) + ( len <*(x + y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm17, Lm59;

    end;

    theorem :: O_RING_1:9

    x is being_an_amalgam_of_squares & (y is being_a_product_of_squares or y is being_an_amalgam_of_squares) or x is being_a_sum_of_amalgams_of_squares & (y is being_a_square or y is being_a_product_of_squares or y is being_an_amalgam_of_squares) implies (x + y) is being_a_sum_of_amalgams_of_squares by Lm60, Lm66, Lm67, Lm68, Lm69;

    

     Lm70: x is being_a_square & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_square & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm38;

      hence thesis by Lm64;

    end;

    

     Lm71: x is being_a_square & y is being_a_product_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_square & y is being_a_product_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm49;

      hence thesis by Lm64;

    end;

    

     Lm72: x is being_a_square & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_square and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm31;

      hence thesis by A2, Lm64;

    end;

    

     Lm73: x is being_a_square & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_square & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm54;

      hence thesis by Lm64;

    end;

    

     Lm74: x is being_a_square & y is being_an_amalgam_of_squares implies (x + y) is generated_from_squares by Lm40, Lm72;

    

     Lm75: x is being_a_square & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares by Lm72, Th1;

    theorem :: O_RING_1:10

    x is being_a_square & (y is being_a_sum_of_squares or y is being_a_product_of_squares or y is being_a_sum_of_products_of_squares or y is being_an_amalgam_of_squares or y is being_a_sum_of_amalgams_of_squares or y is generated_from_squares) implies (x + y) is generated_from_squares by Lm70, Lm71, Lm72, Lm73, Lm74, Lm75;

    theorem :: O_RING_1:11

    x is being_a_sum_of_squares & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:12

    x is being_a_sum_of_squares & y is being_a_product_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_product_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm49;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:13

    x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm54;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:14

    x is being_a_sum_of_squares & y is being_an_amalgam_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_an_amalgam_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm40;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:15

    x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:16

    x is being_a_sum_of_squares & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_sum_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm38;

      hence thesis by A2, Lm64;

    end;

    theorem :: O_RING_1:17

    x is being_a_product_of_squares & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_product_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm49;

      hence thesis by A2, Lm64;

    end;

    theorem :: O_RING_1:18

    x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49, Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:19

    x is being_a_product_of_squares & y is being_an_amalgam_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_an_amalgam_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Lm49;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:20

    x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49, Lm54;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:21

    x is being_a_product_of_squares & y is being_a_product_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_product_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:22

    x is being_a_product_of_squares & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm49;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:23

    x is being_a_product_of_squares & y is being_a_square implies (x + y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_square;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm49;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:24

    x is being_a_sum_of_products_of_squares & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_sum_of_products_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm54;

      hence thesis by A2, Lm64;

    end;

    theorem :: O_RING_1:25

    x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm54;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:26

    x is being_a_sum_of_products_of_squares & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm54;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:27

    x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Lm54;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:28

    x is being_a_sum_of_products_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm54, Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:29

    x is being_an_amalgam_of_squares & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm40;

      hence thesis by A2, Lm64;

    end;

    theorem :: O_RING_1:30

    x is being_an_amalgam_of_squares & y is being_a_square implies (x + y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_square;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm40;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:31

    x is being_an_amalgam_of_squares & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm40;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:32

    x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Lm54;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:33

    x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:34

    x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:35

    x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm54, Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:36

    x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Th1;

      hence thesis by Lm64;

    end;

    theorem :: O_RING_1:37

    x is being_a_sum_of_amalgams_of_squares & y is generated_from_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_sum_of_amalgams_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Th1;

      hence thesis by A2, Lm64;

    end;

    

     Lm76: x is generated_from_squares & y is being_a_sum_of_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_sum_of_squares;

      y is generated_from_squares by A2, Lm38;

      hence thesis by A1, Lm64;

    end;

    

     Lm77: x is generated_from_squares & y is being_a_product_of_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_product_of_squares;

      y is generated_from_squares by A2, Lm49;

      hence thesis by A1, Lm64;

    end;

    

     Lm78: x is generated_from_squares & y is being_a_sum_of_products_of_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_sum_of_products_of_squares;

      y is generated_from_squares by A2, Lm54;

      hence thesis by A1, Lm64;

    end;

    

     Lm79: x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares implies (x + y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_sum_of_amalgams_of_squares;

      y is generated_from_squares by A2, Th1;

      hence thesis by A1, Lm64;

    end;

    theorem :: O_RING_1:38

    x is generated_from_squares & y is being_a_square or x is generated_from_squares & y is being_a_sum_of_squares or x is generated_from_squares & y is being_a_product_of_squares or x is generated_from_squares & y is being_a_sum_of_products_of_squares or x is generated_from_squares & y is being_an_amalgam_of_squares or x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares or x is generated_from_squares & y is generated_from_squares implies (x + y) is generated_from_squares by Lm36, Lm43, Lm64, Lm76, Lm77, Lm78, Lm79;

    begin

    

     Lm80: f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares implies (f ^ g) is being_an_Amalgam_of_squares

    proof

      assume that

       A1: f is being_an_Amalgam_of_squares and

       A2: g is being_an_Amalgam_of_squares;

      

       A3: for n st n <> 0 & n <= ( len (f ^ g)) holds ((f ^ g) /. n) is being_a_product_of_squares or ex i, j st ((f ^ g) /. n) = (((f ^ g) /. i) * ((f ^ g) /. j)) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n;

        assume that

         A4: n <> 0 and

         A5: n <= ( len (f ^ g));

        

         A6: n <= (( len f) + ( len g)) by A5, FINSEQ_1: 22;

         A7:

        now

          assume

           A8: ( len f) < n;

          then

          consider m be Nat such that

           A9: n = (( len f) + m) by NAT_1: 10;

          (( len f) + m) <= (( len f) + ( len g)) by A5, A9, FINSEQ_1: 22;

          then

           A10: m <= ( len g) by XREAL_1: 6;

          

           A11: m <> 0 by A8, A9;

          

           A12: m <= ( len g) by A6, A9, XREAL_1: 6;

           A13:

          now

            given k,l be Nat such that

             A14: (g /. m) = ((g /. k) * (g /. l)) and

             A15: k <> 0 and

             A16: k < m and

             A17: l <> 0 and

             A18: l < m;

            

             A19: (( len f) + k) <> 0 & (( len f) + l) <> 0 by A15, A17;

            

             A20: (( len f) + k) < n & (( len f) + l) < n by A9, A16, A18, XREAL_1: 6;

            ((f ^ g) /. n) = ((g /. k) * (g /. l)) by A9, A11, A10, A14, Lm5

            .= (((f ^ g) /. (( len f) + k)) * (g /. l)) by A12, A15, A16, Lm5, XXREAL_0: 2

            .= (((f ^ g) /. (( len f) + k)) * ((f ^ g) /. (( len f) + l))) by A12, A17, A18, Lm5, XXREAL_0: 2;

            hence thesis by A19, A20;

          end;

          (g /. m) is being_a_product_of_squares implies thesis by A9, A11, A10, Lm5;

          hence thesis by A2, A11, A10, A13;

        end;

        now

          assume

           A21: n <= ( len f);

           A22:

          now

            given k,l be Nat such that

             A23: (f /. n) = ((f /. k) * (f /. l)) and

             A24: k <> 0 & k < n and

             A25: l <> 0 & l < n;

            ((f ^ g) /. n) = ((f /. k) * (f /. l)) by A4, A21, A23, Lm4

            .= (((f ^ g) /. k) * (f /. l)) by A21, A24, Lm4, XXREAL_0: 2

            .= (((f ^ g) /. k) * ((f ^ g) /. l)) by A21, A25, Lm4, XXREAL_0: 2;

            hence thesis by A24, A25;

          end;

          (f /. n) is being_a_product_of_squares implies thesis by A4, A21, Lm4;

          hence thesis by A1, A4, A21, A22;

        end;

        hence thesis by A7;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len g)) <> 0 ;

      then ( len (f ^ g)) <> 0 by FINSEQ_1: 22;

      hence thesis by A3;

    end;

    

     Lm81: f is being_an_Amalgam_of_squares & i <> 0 & i <= ( len f) & j <> 0 & j <= ( len f) implies (f ^ <*((f /. i) * (f /. j))*>) is being_an_Amalgam_of_squares

    proof

      assume that

       A1: f is being_an_Amalgam_of_squares and

       A2: i <> 0 and

       A3: i <= ( len f) and

       A4: j <> 0 and

       A5: j <= ( len f);

      set g = (f ^ <*((f /. i) * (f /. j))*>);

      

       A6: ( len g) = (( len f) + ( len <*((f /. i) * (f /. j))*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A7: for n st n <> 0 & n <= ( len g) holds (g /. n) is being_a_product_of_squares or ex i, j st (g /. n) = ((g /. i) * (g /. j)) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A8: n <> 0 and

         A9: n <= ( len g);

         A10:

        now

          assume n < ( len g);

          then

           A11: n <= ( len f) by A6, NAT_1: 13;

           A12:

          now

            given k,m be Nat such that

             A13: (f /. n) = ((f /. k) * (f /. m)) and

             A14: k <> 0 & k < n and

             A15: m <> 0 & m < n;

            (g /. n) = ((f /. k) * (f /. m)) by A8, A11, A13, Lm4

            .= ((g /. k) * (f /. m)) by A11, A14, Lm4, XXREAL_0: 2

            .= ((g /. k) * (g /. m)) by A11, A15, Lm4, XXREAL_0: 2;

            hence thesis by A14, A15;

          end;

          (f /. n) is being_a_product_of_squares implies thesis by A8, A11, Lm4;

          hence thesis by A1, A8, A11, A12;

        end;

        now

          assume

           A16: n = ( len g);

          then

           A17: i < n & j < n by A3, A5, A6, NAT_1: 13;

          (g /. n) = ((f /. i) * (f /. j)) by A6, A16, Lm3

          .= ((g /. i) * (f /. j)) by A2, A3, Lm4

          .= ((g /. i) * (g /. j)) by A4, A5, Lm4;

          hence thesis by A2, A4, A17;

        end;

        hence thesis by A9, A10, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len <*((f /. i) * (f /. j))*>)) <> 0 ;

      then ( len (f ^ <*((f /. i) * (f /. j))*>)) <> 0 by FINSEQ_1: 22;

      hence thesis by A7;

    end;

    

     Lm82: f is being_a_generation_from_squares & i <> 0 & i <= ( len f) & j <> 0 & j <= ( len f) implies (f ^ <*((f /. i) * (f /. j))*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: i <> 0 and

       A3: i <= ( len f) and

       A4: j <> 0 and

       A5: j <= ( len f);

      set g = (f ^ <*((f /. i) * (f /. j))*>);

      

       A6: ( len g) = (( len f) + ( len <*((f /. i) * (f /. j))*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A7: for n st n <> 0 & n <= ( len g) holds (g /. n) is being_an_amalgam_of_squares or ex i, j st ((g /. n) = ((g /. i) * (g /. j)) or (g /. n) = ((g /. i) + (g /. j))) & i <> 0 & i < n & j <> 0 & j < n

      proof

        let n such that

         A8: n <> 0 and

         A9: n <= ( len g);

         A10:

        now

          assume n < ( len g);

          then

           A11: n <= ( len f) by A6, NAT_1: 13;

          then

           A12: (g /. n) = (f /. n) by A8, Lm4;

           A13:

          now

            given k,m be Nat such that

             A14: (f /. n) = ((f /. k) * (f /. m)) or (f /. n) = ((f /. k) + (f /. m)) and

             A15: k <> 0 & k < n & m <> 0 & m < n;

            (f /. k) = (g /. k) & (f /. m) = (g /. m) by A11, A15, Lm4, XXREAL_0: 2;

            hence thesis by A12, A14, A15;

          end;

          (f /. n) is being_an_amalgam_of_squares implies thesis by A8, A11, Lm4;

          hence thesis by A1, A8, A11, A13;

        end;

        now

          assume

           A16: n = ( len g);

          then

           A17: i < n & j < n by A3, A5, A6, NAT_1: 13;

          (g /. n) = ((f /. i) * (f /. j)) by A6, A16, Lm3

          .= ((g /. i) * (f /. j)) by A2, A3, Lm4

          .= ((g /. i) * (g /. j)) by A4, A5, Lm4;

          hence thesis by A2, A4, A17;

        end;

        hence thesis by A9, A10, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then (( len f) + ( len <*((f /. i) * (f /. j))*>)) <> 0 ;

      then ( len (f ^ <*((f /. i) * (f /. j))*>)) <> 0 by FINSEQ_1: 22;

      hence thesis by A7;

    end;

    

     Lm83: f is being_a_Product_of_squares & x is being_a_square implies (f ^ <*((f /. ( len f)) * x)*>) is being_a_Product_of_squares

    proof

      assume that

       A1: f is being_a_Product_of_squares and

       A2: x is being_a_square;

      set g = (f ^ <*((f /. ( len f)) * x)*>);

      

       A3: ( len g) = (( len f) + ( len <*((f /. ( len f)) * x)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      

       A4: for n st n <> 0 & n < ( len g) holds (f /. n) = (g /. n)

      proof

        let n;

        assume n <> 0 & n < ( len g);

        then 1 <= n & n <= ( len f) by A3, NAT_1: 13, NAT_1: 25;

        then n in ( dom f) by FINSEQ_3: 25;

        hence thesis by Lm1;

      end;

      

       A5: for n st n <> 0 & n < ( len g) holds ex y st y is being_a_square & (g /. (n + 1)) = ((g /. n) * y)

      proof

        let n;

        assume that

         A6: n <> 0 and

         A7: n < ( len g);

         A8:

        now

          

           A9: (f /. n) = (g /. n) by A4, A6, A7;

          assume

           A10: n < ( len f);

          then (n + 1) <> 0 & (n + 1) < ( len g) by A3, XREAL_1: 6;

          then (f /. (n + 1)) = (g /. (n + 1)) by A4;

          hence thesis by A1, A6, A10, A9;

        end;

         A11:

        now

          assume

           A12: n = ( len f);

          1 <= n by A6, NAT_1: 25;

          then

           A13: n in ( dom f) by A12, FINSEQ_3: 25;

          (g /. (n + 1)) = ((f /. n) * x) by A12, Lm3;

          then (g /. (n + 1)) = ((g /. n) * x) by A13, Lm1;

          hence thesis by A2;

        end;

        n <= ( len f) by A3, A7, NAT_1: 13;

        hence thesis by A8, A11, XXREAL_0: 1;

      end;

      ( len f) <> 0 by A1;

      then 1 <= ( len f) by NAT_1: 25;

      then 1 < ( len g) by A3, NAT_1: 13;

      then (g /. 1) = (f /. 1) by A4;

      then

       A14: (g /. 1) is being_a_square by A1;

      ( len g) <> 0 by A3;

      hence thesis by A14, A5;

    end;

    

     Lm84: f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares implies ((f ^ g) ^ <*((f /. ( len f)) * (g /. ( len g)))*>) is being_an_Amalgam_of_squares

    proof

      assume that

       A1: f is being_an_Amalgam_of_squares and

       A2: g is being_an_Amalgam_of_squares;

      ( len f) <> 0 by A1;

      then

       A3: (( len f) + ( len g)) <= ( len (f ^ g)) & ((f ^ g) /. ( len f)) = (f /. ( len f)) by Lm4, FINSEQ_1: 22;

      ( len g) <> 0 by A2;

      then

       A4: (( len f) + ( len g)) <> 0 & ((f ^ g) /. (( len f) + ( len g))) = (g /. ( len g)) by Lm5;

      ( len f) <= (( len f) + ( len g)) by NAT_1: 11;

      then

       A5: ( len f) <= ( len (f ^ g)) by FINSEQ_1: 22;

      ( len f) <> 0 & (f ^ g) is being_an_Amalgam_of_squares by A1, A2, Lm80;

      hence thesis by A5, A3, A4, Lm81;

    end;

    

     Lm85: f is being_a_generation_from_squares & g is being_a_generation_from_squares implies ((f ^ g) ^ <*((f /. ( len f)) * (g /. ( len g)))*>) is being_a_generation_from_squares

    proof

      assume that

       A1: f is being_a_generation_from_squares and

       A2: g is being_a_generation_from_squares;

      

       A3: ( len g) <> 0 by A2;

      ( len f) <> 0 by A1;

      then 1 <= ( len f) by NAT_1: 25;

      then ( len f) in ( dom f) by FINSEQ_3: 25;

      then

       A4: (( len f) + ( len g)) <= ( len (f ^ g)) & ((f ^ g) /. ( len f)) = (f /. ( len f)) by Lm1, FINSEQ_1: 22;

      ( len f) <= (( len f) + ( len g)) by NAT_1: 11;

      then

       A5: ( len f) <= ( len (f ^ g)) by FINSEQ_1: 22;

      1 <= ( len g) by A3, NAT_1: 25;

      then ( len g) in ( dom g) by FINSEQ_3: 25;

      then

       A6: ((f ^ g) /. (( len f) + ( len g))) = (g /. ( len g)) by Lm1;

      (f ^ g) is being_a_generation_from_squares & ( len f) <> 0 by A1, A2, Lm33;

      hence thesis by A5, A4, A6, Lm82;

    end;

    theorem :: O_RING_1:39

    x is being_a_product_of_squares & y is being_a_square implies (x * y) is being_a_product_of_squares

    proof

      assume that

       A1: x is being_a_product_of_squares and

       A2: y is being_a_square;

      consider f such that

       A3: f is being_a_Product_of_squares & x = (f /. ( len f)) by A1;

      take g = (f ^ <*(x * y)*>);

      ( len g) = (( len f) + ( len <*(x * y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm83;

    end;

    theorem :: O_RING_1:40

    x is being_a_square & y is being_a_square implies (x * y) is being_a_product_of_squares

    proof

      assume that

       A1: x is being_a_square and

       A2: y is being_a_square;

      x is being_a_product_of_squares by A1, Lm9;

      then

      consider f such that

       A3: f is being_a_Product_of_squares & x = (f /. ( len f));

      take g = (f ^ <*(x * y)*>);

      ( len g) = (( len f) + ( len <*(x * y)*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by Lm2;

      hence thesis by A2, A3, Lm3, Lm83;

    end;

    

     Lm86: x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares implies (x * y) is being_an_amalgam_of_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is being_an_amalgam_of_squares;

      consider f such that

       A3: f is being_an_Amalgam_of_squares & x = (f /. ( len f)) by A1;

      consider g such that

       A4: g is being_an_Amalgam_of_squares & y = (g /. ( len g)) by A2;

      take h = ((f ^ g) ^ <*((f /. ( len f)) * (g /. ( len g)))*>);

      ( len h) = (( len (f ^ g)) + ( len <*((f /. ( len f)) * (g /. ( len g)))*>)) by FINSEQ_1: 22

      .= (( len (f ^ g)) + 1) by Lm2;

      hence thesis by A3, A4, Lm3, Lm84;

    end;

    theorem :: O_RING_1:41

    x is being_a_square & y is being_a_product_of_squares implies (x * y) is being_an_amalgam_of_squares

    proof

      assume x is being_a_square & y is being_a_product_of_squares;

      then x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares by Lm17, Lm19;

      hence thesis by Lm86;

    end;

    theorem :: O_RING_1:42

    x is being_a_square & y is being_an_amalgam_of_squares implies (x * y) is being_an_amalgam_of_squares

    proof

      assume that

       A1: x is being_a_square and

       A2: y is being_an_amalgam_of_squares;

      x is being_an_amalgam_of_squares by A1, Lm17;

      hence thesis by A2, Lm86;

    end;

    theorem :: O_RING_1:43

    x is being_a_product_of_squares & y is being_a_product_of_squares implies (x * y) is being_an_amalgam_of_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_product_of_squares;

      then x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares by Lm19;

      hence thesis by Lm86;

    end;

    theorem :: O_RING_1:44

    x is being_a_product_of_squares & y is being_an_amalgam_of_squares implies (x * y) is being_an_amalgam_of_squares

    proof

      assume that

       A1: x is being_a_product_of_squares and

       A2: y is being_an_amalgam_of_squares;

      x is being_an_amalgam_of_squares by A1, Lm19;

      hence thesis by A2, Lm86;

    end;

    theorem :: O_RING_1:45

    x is being_an_amalgam_of_squares & y is being_a_square implies (x * y) is being_an_amalgam_of_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is being_a_square;

      y is being_an_amalgam_of_squares by A2, Lm17;

      hence thesis by A1, Lm86;

    end;

    theorem :: O_RING_1:46

    x is being_an_amalgam_of_squares & y is being_a_product_of_squares implies (x * y) is being_an_amalgam_of_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is being_a_product_of_squares;

      y is being_an_amalgam_of_squares by A2, Lm19;

      hence thesis by A1, Lm86;

    end;

    theorem :: O_RING_1:47

    x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares implies (x * y) is being_an_amalgam_of_squares by Lm86;

    

     Lm87: x is generated_from_squares & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is generated_from_squares;

      consider f such that

       A3: f is being_a_generation_from_squares and

       A4: x = (f /. ( len f)) by A1;

      consider g such that

       A5: g is being_a_generation_from_squares and

       A6: y = (g /. ( len g)) by A2;

      set h = ((f ^ g) ^ <*((f /. ( len f)) * (g /. ( len g)))*>);

      ( len h) = (( len (f ^ g)) + ( len <*((f /. ( len f)) * (g /. ( len g)))*>)) by FINSEQ_1: 22

      .= (( len (f ^ g)) + 1) by Lm2;

      then

       A7: (h /. ( len h)) = (x * (g /. ( len g))) by A4, Lm3;

      h is being_a_generation_from_squares by A3, A5, Lm85;

      hence thesis by A6, A7;

    end;

    theorem :: O_RING_1:48

    x is being_a_square & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_square & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm38;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:49

    x is being_a_square & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_square & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:50

    x is being_a_square & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_square & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:51

    x is being_a_square & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_square and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm31;

      hence thesis by A2, Lm87;

    end;

    theorem :: O_RING_1:52

    x is being_a_sum_of_squares & y is being_a_square implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_square;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm38;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:53

    x is being_a_sum_of_squares & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:54

    x is being_a_sum_of_squares & y is being_a_product_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_product_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm49;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:55

    x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:56

    x is being_a_sum_of_squares & y is being_an_amalgam_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_an_amalgam_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm40;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:57

    x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:58

    x is being_a_sum_of_squares & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_sum_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm38;

      hence thesis by A2, Lm87;

    end;

    theorem :: O_RING_1:59

    x is being_a_product_of_squares & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm49;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:60

    x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:61

    x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:62

    x is being_a_product_of_squares & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_product_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm49;

      hence thesis by A2, Lm87;

    end;

    theorem :: O_RING_1:63

    x is being_a_sum_of_products_of_squares & y is being_a_square implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_square;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:64

    x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:65

    x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:66

    x is being_a_sum_of_products_of_squares & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:67

    x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:68

    x is being_a_sum_of_products_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm54, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:69

    x is being_a_sum_of_products_of_squares & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_sum_of_products_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm54;

      hence thesis by A2, Lm87;

    end;

    theorem :: O_RING_1:70

    x is being_an_amalgam_of_squares & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Lm40;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:71

    x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Lm54;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:72

    x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:73

    x is being_an_amalgam_of_squares & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is being_an_amalgam_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Lm40;

      hence thesis by A2, Lm87;

    end;

    theorem :: O_RING_1:74

    x is being_a_sum_of_amalgams_of_squares & y is being_a_square implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_square;

      then x is generated_from_squares & y is generated_from_squares by Lm31, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:75

    x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm38, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:76

    x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm49, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:77

    x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_products_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm54, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:78

    x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Lm40, Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:79

    x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_amalgams_of_squares;

      then x is generated_from_squares & y is generated_from_squares by Th1;

      hence thesis by Lm87;

    end;

    theorem :: O_RING_1:80

    x is being_a_sum_of_amalgams_of_squares & y is generated_from_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is being_a_sum_of_amalgams_of_squares and

       A2: y is generated_from_squares;

      x is generated_from_squares by A1, Th1;

      hence thesis by A2, Lm87;

    end;

    theorem :: O_RING_1:81

    x is generated_from_squares & y is being_a_square implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_square;

      y is generated_from_squares by A2, Lm31;

      hence thesis by A1, Lm87;

    end;

    theorem :: O_RING_1:82

    x is generated_from_squares & y is being_an_amalgam_of_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_an_amalgam_of_squares;

      y is generated_from_squares by A2, Lm40;

      hence thesis by A1, Lm87;

    end;

    theorem :: O_RING_1:83

    x is generated_from_squares & y is being_a_sum_of_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_sum_of_squares;

      y is generated_from_squares by A2, Lm38;

      hence thesis by A1, Lm87;

    end;

    theorem :: O_RING_1:84

    x is generated_from_squares & y is being_a_product_of_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_product_of_squares;

      y is generated_from_squares by A2, Lm49;

      hence thesis by A1, Lm87;

    end;

    theorem :: O_RING_1:85

    x is generated_from_squares & y is being_a_sum_of_products_of_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_sum_of_products_of_squares;

      y is generated_from_squares by A2, Lm54;

      hence thesis by A1, Lm87;

    end;

    theorem :: O_RING_1:86

    x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares implies (x * y) is generated_from_squares

    proof

      assume that

       A1: x is generated_from_squares and

       A2: y is being_a_sum_of_amalgams_of_squares;

      y is generated_from_squares by A2, Th1;

      hence thesis by A1, Lm87;

    end;