:: Ordered Rings - Part I :: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba :: :: Received October 11, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NAT_1, XBOOLE_0, ALGSTR_0, VECTSP_1, FINSEQ_1, ORDINAL4, RELAT_1, ARYTM_3, PARTFUN1, XXREAL_0, CARD_1, FUNCT_1, SQUARE_1, O_RING_1; notations ORDINAL1, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, XXREAL_0; constructors RLVECT_1, PARTFUN1, XXREAL_0, NAT_1, VECTSP_1, RELSET_1, GROUP_1; registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, NAT_1; requirements NUMERALS, SUBSET, ARITHM, BOOLE; theorems NAT_1, FINSEQ_1, FINSEQ_3, XREAL_1, FINSEQ_4, XXREAL_0, PARTFUN1; schemes NAT_1; begin :: Field-like Algebras 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 00 & 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 Scalar of R equals x*x; coherence; end; definition let R be non empty doubleLoopStr, x be Scalar of R; attr x is being_a_square means ex y being Scalar of R st x=y^2; end; definition let R,f; attr f is being_a_Sum_of_squares means len f<>0 & f/.1 is being_a_square & for n st n<>0 & n is being_a_Sum_of_squares proof A1: for n st n<>0 & n 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; 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; attr f is being_a_Product_of_squares means len f<>0 & f/.1 is being_a_square & for n st n<>0 & n is being_a_Product_of_squares proof A1: for n st n<>0 & n 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; 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; 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 is being_a_Sum_of_products_of_squares proof A1: for n st n<>0 & n 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; 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 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; 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 & n0 & n0 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; 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 & i0 & j 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 & i0 & j0 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 & i0 & j0 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; 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 is being_a_Sum_of_amalgams_of_squares proof A1: for n st n<>0 & n 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; 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 & n0 & n0 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 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; 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 & n0 & n0 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 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; 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; 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 & i0 & j 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 & i0 & j0 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 & i0 & j0 and A9: n<=len g; A10: now assume n0 & k0 & m0 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 & i0 & j0 and A5: n<=len (f^g); A6: n<=len f+len g by A5,FINSEQ_1:22; A7: now assume A8: len f0 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: k0 and A18: l0 & 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+k0 & k0 & l0 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: i0; 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 & i0 & j 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 & i0 & j0 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; i0 & 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 & i0 & j0 and A9: n<=len g; A10: now assume n0 & k0 & m0 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: i0; 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 & i0 & j0 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: i0; 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 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 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 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 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 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 :: O_RING_2 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 & n0 & n0 & n0 and A7: n0 & n+10 by A1; then 1<=len f by NAT_1:25; then 10 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 & n0 & n0 & n0 and A7: n0 & n+10 by A1; then 1<=len f by NAT_1:25; then 10 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 & n0 & n0 & n0 and A7: n0 & n+10 by A1; then 1<=len f by NAT_1:25; then 10 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 & i0 & j0 and A9: n<=len g; A10: now assume n0 & k0 & m0 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 :: O_RING_3 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 & i0 & j0 and A5: n<=len (f^g); A6: n<=len f+len g by A5,FINSEQ_1:22; A7: now assume A8: len f0 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: k0 and A18: l0 & len f+l<>0 by A15,A17; A20: len f+k0 & k0 & l0 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 & i0 & j0 and A9: n<=len g; A10: now assume n0 & k0 & m0 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 & i0 & j0 and A9: n<=len g; A10: now assume n0 & k0 & m0 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 & n0 & n0 & n0 and A7: n0 & n+10 by A1; then 1<=len f by NAT_1:25; then 10 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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;