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 ) ) )
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 ) )
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
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
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
:: deftheorem O_RING_1:def 1 :
canceled;
:: deftheorem defines ^2 O_RING_1:def 2 :
for R being non empty doubleLoopStr
for x being Scalar of R holds x ^2 = x * x;
:: deftheorem defines being_a_square O_RING_1:def 3 :
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 );
:: deftheorem Def4 defines being_a_Sum_of_squares O_RING_1:def 4 :
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 ) ) ) );
:: deftheorem Def5 defines being_a_sum_of_squares O_RING_1:def 5 :
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
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
:: deftheorem Def6 defines being_a_Product_of_squares O_RING_1:def 6 :
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 ) ) ) );
:: deftheorem Def7 defines being_a_product_of_squares O_RING_1:def 7 :
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
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
:: deftheorem Def8 defines being_a_Sum_of_products_of_squares O_RING_1:def 8 :
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 ) ) ) );
:: deftheorem Def9 defines being_a_sum_of_products_of_squares O_RING_1:def 9 :
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
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
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
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
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
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
:: deftheorem Def10 defines being_an_Amalgam_of_squares O_RING_1:def 10 :
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 ) ) ) );
:: deftheorem Def11 defines being_an_amalgam_of_squares O_RING_1:def 11 :
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
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
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
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
:: deftheorem Def12 defines being_a_Sum_of_amalgams_of_squares O_RING_1:def 12 :
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 ) ) ) );
:: deftheorem Def13 defines being_a_sum_of_amalgams_of_squares O_RING_1:def 13 :
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
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
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
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
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
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
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
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
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
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
:: deftheorem Def14 defines being_a_generation_from_squares O_RING_1:def 14 :
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 ) ) ) );
:: deftheorem Def15 defines generated_from_squares O_RING_1:def 15 :
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
theorem Th1:
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
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
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
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
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
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
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
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
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
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
theorem
theorem
theorem
theorem
theorem
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
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
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
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
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
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
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
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
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
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
theorem
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
theorem
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
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
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
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
theorem
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
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
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
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
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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
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
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
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
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
theorem
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
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
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
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
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
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
theorem
theorem
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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem