:: Ordered Rings - Part I :: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba :: :: Received October 11, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for R being non empty doubleLoopStr for h, f, g being FinSequence of R holds ( h = f ^ g iff ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds h /. k = f /. k ) & ( for k being Nat st k in dom g holds h /. ((len f) + k) = g /. k ) ) ) proofend; Lm2: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R holds ( f = <*x*> iff ( len f = 1 & f /. 1 = x ) ) proofend; Lm3: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R holds (f ^ <*x*>) /. ((len f) + 1) = x proofend; Lm4: for i being Nat for R being non empty doubleLoopStr for f, g being FinSequence of R st i <> 0 & i <= len f holds (f ^ g) /. i = f /. i proofend; Lm5: for i being Nat for R being non empty doubleLoopStr for g, f being FinSequence of R st i <> 0 & i <= len g holds (f ^ g) /. ((len f) + i) = g /. i proofend; definition let R be non empty doubleLoopStr ; let x be Scalar of R; funcx ^2 -> Scalar of R equals :: O_RING_1:def 1 x * x; coherence x * x is Scalar of R ; end; :: deftheorem defines ^2 O_RING_1:def_1_:_ for R being non empty doubleLoopStr for x being Scalar of R holds x ^2 = x * x; definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is being_a_square means :: O_RING_1:def 2 ex y being Scalar of R st x = y ^2 ; end; :: deftheorem defines being_a_square O_RING_1:def_2_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is being_a_square iff ex y being Scalar of R st x = y ^2 ); definition let R be non empty doubleLoopStr ; let f be FinSequence of R; attrf is being_a_Sum_of_squares means :Def3: :: O_RING_1:def 3 ( len f <> 0 & f /. 1 is being_a_square & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_a_square & f /. (n + 1) = (f /. n) + y ) ) ); end; :: deftheorem Def3 defines being_a_Sum_of_squares O_RING_1:def_3_:_ for R being non empty doubleLoopStr for f being FinSequence of R holds ( f is being_a_Sum_of_squares iff ( len f <> 0 & f /. 1 is being_a_square & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_a_square & f /. (n + 1) = (f /. n) + y ) ) ) ); definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is being_a_sum_of_squares means :Def4: :: O_RING_1:def 4 ex f being FinSequence of R st ( f is being_a_Sum_of_squares & x = f /. (len f) ); end; :: deftheorem Def4 defines being_a_sum_of_squares O_RING_1:def_4_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is being_a_sum_of_squares iff ex f being FinSequence of R st ( f is being_a_Sum_of_squares & x = f /. (len f) ) ); Lm6: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds <*x*> is being_a_Sum_of_squares proofend; Lm7: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds x is being_a_sum_of_squares proofend; definition let R be non empty doubleLoopStr ; let f be FinSequence of R; attrf is being_a_Product_of_squares means :Def5: :: O_RING_1:def 5 ( len f <> 0 & f /. 1 is being_a_square & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_a_square & f /. (n + 1) = (f /. n) * y ) ) ); end; :: deftheorem Def5 defines being_a_Product_of_squares O_RING_1:def_5_:_ for R being non empty doubleLoopStr for f being FinSequence of R holds ( f is being_a_Product_of_squares iff ( len f <> 0 & f /. 1 is being_a_square & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_a_square & f /. (n + 1) = (f /. n) * y ) ) ) ); definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is being_a_product_of_squares means :Def6: :: O_RING_1:def 6 ex f being FinSequence of R st ( f is being_a_Product_of_squares & x = f /. (len f) ); end; :: deftheorem Def6 defines being_a_product_of_squares O_RING_1:def_6_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is being_a_product_of_squares iff ex f being FinSequence of R st ( f is being_a_Product_of_squares & x = f /. (len f) ) ); Lm8: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds <*x*> is being_a_Product_of_squares proofend; Lm9: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds x is being_a_product_of_squares proofend; definition let R be non empty doubleLoopStr ; let f be FinSequence of R; attrf is being_a_Sum_of_products_of_squares means :Def7: :: O_RING_1:def 7 ( len f <> 0 & f /. 1 is being_a_product_of_squares & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y ) ) ); end; :: deftheorem Def7 defines being_a_Sum_of_products_of_squares O_RING_1:def_7_:_ for R being non empty doubleLoopStr for f being FinSequence of R holds ( f is being_a_Sum_of_products_of_squares iff ( len f <> 0 & f /. 1 is being_a_product_of_squares & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y ) ) ) ); definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is being_a_sum_of_products_of_squares means :Def8: :: O_RING_1:def 8 ex f being FinSequence of R st ( f is being_a_Sum_of_products_of_squares & x = f /. (len f) ); end; :: deftheorem Def8 defines being_a_sum_of_products_of_squares O_RING_1:def_8_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is being_a_sum_of_products_of_squares iff ex f being FinSequence of R st ( f is being_a_Sum_of_products_of_squares & x = f /. (len f) ) ); Lm10: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds <*x*> is being_a_Sum_of_products_of_squares proofend; Lm11: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds x is being_a_sum_of_products_of_squares proofend; Lm12: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds <*x*> is being_a_Sum_of_products_of_squares proofend; Lm13: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds x is being_a_sum_of_products_of_squares proofend; Lm14: for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Sum_of_squares holds f is being_a_Sum_of_products_of_squares proofend; Lm15: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_squares holds x is being_a_sum_of_products_of_squares proofend; definition let R be non empty doubleLoopStr ; let f be FinSequence of R; attrf is being_an_Amalgam_of_squares means :Def9: :: O_RING_1:def 9 ( len f <> 0 & ( for n being Nat st n <> 0 & n <= len f & not f /. n is being_a_product_of_squares holds ex i, j being Nat st ( f /. n = (f /. i) * (f /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) ); end; :: deftheorem Def9 defines being_an_Amalgam_of_squares O_RING_1:def_9_:_ for R being non empty doubleLoopStr for f being FinSequence of R holds ( f is being_an_Amalgam_of_squares iff ( len f <> 0 & ( for n being Nat st n <> 0 & n <= len f & not f /. n is being_a_product_of_squares holds ex i, j being Nat st ( f /. n = (f /. i) * (f /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) ) ); definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is being_an_amalgam_of_squares means :Def10: :: O_RING_1:def 10 ex f being FinSequence of R st ( f is being_an_Amalgam_of_squares & x = f /. (len f) ); end; :: deftheorem Def10 defines being_an_amalgam_of_squares O_RING_1:def_10_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is being_an_amalgam_of_squares iff ex f being FinSequence of R st ( f is being_an_Amalgam_of_squares & x = f /. (len f) ) ); Lm16: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds <*x*> is being_an_Amalgam_of_squares proofend; Lm17: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds x is being_an_amalgam_of_squares proofend; Lm18: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds <*x*> is being_an_Amalgam_of_squares proofend; Lm19: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds x is being_an_amalgam_of_squares proofend; definition let R be non empty doubleLoopStr ; let f be FinSequence of R; attrf is being_a_Sum_of_amalgams_of_squares means :Def11: :: O_RING_1:def 11 ( len f <> 0 & f /. 1 is being_an_amalgam_of_squares & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_an_amalgam_of_squares & f /. (n + 1) = (f /. n) + y ) ) ); end; :: deftheorem Def11 defines being_a_Sum_of_amalgams_of_squares O_RING_1:def_11_:_ for R being non empty doubleLoopStr for f being FinSequence of R holds ( f is being_a_Sum_of_amalgams_of_squares iff ( len f <> 0 & f /. 1 is being_an_amalgam_of_squares & ( for n being Nat st n <> 0 & n < len f holds ex y being Scalar of R st ( y is being_an_amalgam_of_squares & f /. (n + 1) = (f /. n) + y ) ) ) ); definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is being_a_sum_of_amalgams_of_squares means :Def12: :: O_RING_1:def 12 ex f being FinSequence of R st ( f is being_a_Sum_of_amalgams_of_squares & x = f /. (len f) ); end; :: deftheorem Def12 defines being_a_sum_of_amalgams_of_squares O_RING_1:def_12_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is being_a_sum_of_amalgams_of_squares iff ex f being FinSequence of R st ( f is being_a_Sum_of_amalgams_of_squares & x = f /. (len f) ) ); Lm20: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds <*x*> is being_a_Sum_of_amalgams_of_squares proofend; Lm21: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds x is being_a_sum_of_amalgams_of_squares proofend; Lm22: for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Sum_of_squares holds f is being_a_Sum_of_amalgams_of_squares proofend; Lm23: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_squares holds x is being_a_sum_of_amalgams_of_squares proofend; Lm24: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds <*x*> is being_a_Sum_of_amalgams_of_squares proofend; Lm25: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds x is being_a_sum_of_amalgams_of_squares proofend; Lm26: for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Sum_of_products_of_squares holds f is being_a_Sum_of_amalgams_of_squares proofend; Lm27: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_products_of_squares holds x is being_a_sum_of_amalgams_of_squares proofend; Lm28: for R being non empty doubleLoopStr for x being Scalar of R st x is being_an_amalgam_of_squares holds <*x*> is being_a_Sum_of_amalgams_of_squares proofend; Lm29: for R being non empty doubleLoopStr for x being Scalar of R st x is being_an_amalgam_of_squares holds x is being_a_sum_of_amalgams_of_squares proofend; definition let R be non empty doubleLoopStr ; let f be FinSequence of R; attrf is being_a_generation_from_squares means :Def13: :: O_RING_1:def 13 ( len f <> 0 & ( for n being Nat st n <> 0 & n <= len f & not f /. n is being_an_amalgam_of_squares holds ex i, j being Nat st ( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) ); end; :: deftheorem Def13 defines being_a_generation_from_squares O_RING_1:def_13_:_ for R being non empty doubleLoopStr for f being FinSequence of R holds ( f is being_a_generation_from_squares iff ( len f <> 0 & ( for n being Nat st n <> 0 & n <= len f & not f /. n is being_an_amalgam_of_squares holds ex i, j being Nat st ( ( f /. n = (f /. i) * (f /. j) or f /. n = (f /. i) + (f /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) ) ); definition let R be non empty doubleLoopStr ; let x be Scalar of R; attrx is generated_from_squares means :Def14: :: O_RING_1:def 14 ex f being FinSequence of R st ( f is being_a_generation_from_squares & x = f /. (len f) ); end; :: deftheorem Def14 defines generated_from_squares O_RING_1:def_14_:_ for R being non empty doubleLoopStr for x being Scalar of R holds ( x is generated_from_squares iff ex f being FinSequence of R st ( f is being_a_generation_from_squares & x = f /. (len f) ) ); Lm30: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds <*x*> is being_a_generation_from_squares proofend; Lm31: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds x is generated_from_squares proofend; Lm32: for i, j being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares proofend; Lm33: for R being non empty doubleLoopStr for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds f ^ g is being_a_generation_from_squares proofend; Lm34: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds f ^ <*x*> is being_a_generation_from_squares proofend; Lm35: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds (f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares proofend; Lm36: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_square holds x + y is generated_from_squares proofend; Lm37: for i being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Sum_of_squares & 0 <> i & i <= len f holds f /. i is generated_from_squares proofend; Lm38: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_squares holds x is generated_from_squares proofend; Lm39: for R being non empty doubleLoopStr for f being FinSequence of R st f is being_an_Amalgam_of_squares holds f is being_a_generation_from_squares proofend; Lm40: for R being non empty doubleLoopStr for x being Scalar of R st x is being_an_amalgam_of_squares holds x is generated_from_squares proofend; Lm41: for R being non empty doubleLoopStr for x being Scalar of R st x is being_an_amalgam_of_squares holds <*x*> is being_a_generation_from_squares proofend; Lm42: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_generation_from_squares & x is being_an_amalgam_of_squares holds (f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares proofend; Lm43: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_an_amalgam_of_squares holds x + y is generated_from_squares proofend; Lm44: for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Sum_of_amalgams_of_squares holds for i being Nat st i <> 0 & i <= len f holds f /. i is generated_from_squares proofend; theorem Th1: :: O_RING_1:1 for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_amalgams_of_squares holds x is generated_from_squares proofend; Lm45: for i, j being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares proofend; Lm46: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds (f ^ <*x*>) ^ <*((f /. (len f)) * x)*> is being_a_generation_from_squares proofend; Lm47: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_square holds x * y is generated_from_squares proofend; Lm48: for i being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Product_of_squares & 0 <> i & i <= len f holds f /. i is generated_from_squares proofend; Lm49: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds x is generated_from_squares proofend; Lm50: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds <*x*> is being_a_generation_from_squares proofend; Lm51: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_product_of_squares holds (f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares proofend; Lm52: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_product_of_squares holds x + y is generated_from_squares proofend; Lm53: for i being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_Sum_of_products_of_squares & 0 <> i & i <= len f holds f /. i is generated_from_squares proofend; Lm54: for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_products_of_squares holds x is generated_from_squares proofend; theorem :: O_RING_1:2 for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_square holds ( 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 for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_squares holds ( 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 for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_product_of_squares holds ( 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 for R being non empty doubleLoopStr for x being Scalar of R st x is being_a_sum_of_products_of_squares holds ( x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares ) by Lm27, Lm54; theorem :: O_RING_1:6 for R being non empty doubleLoopStr for x being Scalar of R st x is being_an_amalgam_of_squares holds ( x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares ) by Lm29, Lm40; begin Lm55: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_Sum_of_squares & x is being_a_square holds f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_squares proofend; Lm56: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_square holds x + y is being_a_sum_of_squares proofend; Lm57: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_Sum_of_products_of_squares & x is being_a_product_of_squares holds f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares proofend; Lm58: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares holds x + y is being_a_sum_of_products_of_squares proofend; Lm59: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_Sum_of_amalgams_of_squares & x is being_an_amalgam_of_squares holds f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_amalgams_of_squares proofend; Lm60: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares holds x + y is being_a_sum_of_amalgams_of_squares proofend; Lm61: for i, j being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares proofend; Lm62: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_square holds x + y is being_a_sum_of_squares proofend; Lm63: for R being non empty doubleLoopStr for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds (f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares proofend; Lm64: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is generated_from_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:7 for R being non empty doubleLoopStr for x, y being Scalar of R st ( ( x is being_a_square & y is being_a_square ) or ( x is being_a_sum_of_squares & y is being_a_square ) ) holds x + y is being_a_sum_of_squares by Lm56, Lm62; Lm65: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_square holds x + y is being_a_sum_of_products_of_squares proofend; theorem :: O_RING_1:8 for R being non empty doubleLoopStr for x, y being Scalar of R st ( ( 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 ) ) holds x + y is being_a_sum_of_products_of_squares by Lm58, Lm65; Lm66: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_product_of_squares holds x + y is being_a_sum_of_amalgams_of_squares proofend; Lm67: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares holds x + y is being_a_sum_of_amalgams_of_squares proofend; Lm68: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares holds x + y is being_a_sum_of_amalgams_of_squares proofend; Lm69: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_square holds x + y is being_a_sum_of_amalgams_of_squares proofend; theorem :: O_RING_1:9 for R being non empty doubleLoopStr for x, y being Scalar of R st ( ( 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 ) ) ) holds x + y is being_a_sum_of_amalgams_of_squares by Lm60, Lm66, Lm67, Lm68, Lm69; Lm70: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; Lm71: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_product_of_squares holds x + y is generated_from_squares proofend; Lm72: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is generated_from_squares holds x + y is generated_from_squares proofend; Lm73: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; Lm74: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_an_amalgam_of_squares holds x + y is generated_from_squares by Lm40, Lm72; Lm75: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares by Lm72, Th1; theorem :: O_RING_1:10 for R being non empty doubleLoopStr for x, y being Scalar of R st 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 ) holds x + y is generated_from_squares by Lm70, Lm71, Lm72, Lm73, Lm74, Lm75; theorem :: O_RING_1:11 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:12 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_product_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:13 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:14 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_an_amalgam_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:15 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:16 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is generated_from_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:17 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is generated_from_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:18 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:19 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_an_amalgam_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:20 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:21 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_product_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:22 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:23 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_square holds x + y is generated_from_squares proofend; theorem :: O_RING_1:24 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is generated_from_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:25 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:26 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:27 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:28 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:29 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is generated_from_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:30 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_square holds x + y is generated_from_squares proofend; theorem :: O_RING_1:31 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:32 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:33 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:34 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:35 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:36 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:37 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is generated_from_squares holds x + y is generated_from_squares proofend; Lm76: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_squares holds x + y is generated_from_squares proofend; Lm77: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_product_of_squares holds x + y is generated_from_squares proofend; Lm78: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_products_of_squares holds x + y is generated_from_squares proofend; Lm79: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares holds x + y is generated_from_squares proofend; theorem :: O_RING_1:38 for R being non empty doubleLoopStr for x, y being Scalar of R st ( ( 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 ) ) holds x + y is generated_from_squares by Lm36, Lm43, Lm64, Lm76, Lm77, Lm78, Lm79; begin Lm80: for R being non empty doubleLoopStr for f, g being FinSequence of R st f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares holds f ^ g is being_an_Amalgam_of_squares proofend; Lm81: for i, j being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares proofend; Lm82: for i, j being Nat for R being non empty doubleLoopStr for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares proofend; Lm83: for R being non empty doubleLoopStr for x being Scalar of R for f being FinSequence of R st f is being_a_Product_of_squares & x is being_a_square holds f ^ <*((f /. (len f)) * x)*> is being_a_Product_of_squares proofend; Lm84: for R being non empty doubleLoopStr for f, g being FinSequence of R st f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares holds (f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_an_Amalgam_of_squares proofend; Lm85: for R being non empty doubleLoopStr for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds (f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_a_generation_from_squares proofend; theorem :: O_RING_1:39 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_square holds x * y is being_a_product_of_squares proofend; theorem :: O_RING_1:40 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_square holds x * y is being_a_product_of_squares proofend; Lm86: for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:41 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_product_of_squares holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:42 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_an_amalgam_of_squares holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:43 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_product_of_squares holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:44 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_an_amalgam_of_squares holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:45 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_square holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:46 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_product_of_squares holds x * y is being_an_amalgam_of_squares proofend; theorem :: O_RING_1:47 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares holds x * y is being_an_amalgam_of_squares by Lm86; Lm87: for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:48 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:49 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:50 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:51 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_square & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:52 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_square holds x * y is generated_from_squares proofend; theorem :: O_RING_1:53 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:54 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_product_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:55 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:56 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_an_amalgam_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:57 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:58 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_squares & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:59 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:60 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:61 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:62 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_product_of_squares & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:63 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_square holds x * y is generated_from_squares proofend; theorem :: O_RING_1:64 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:65 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:66 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:67 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:68 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:69 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:70 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:71 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:72 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:73 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:74 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_square holds x * y is generated_from_squares proofend; theorem :: O_RING_1:75 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:76 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:77 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:78 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:79 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:80 for R being non empty doubleLoopStr for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is generated_from_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:81 for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_square holds x * y is generated_from_squares proofend; theorem :: O_RING_1:82 for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_an_amalgam_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:83 for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:84 for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_product_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:85 for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_products_of_squares holds x * y is generated_from_squares proofend; theorem :: O_RING_1:86 for R being non empty doubleLoopStr for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares holds x * y is generated_from_squares proofend;