:: Ordered Rings - Part I
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for R being non empty doubleLoopStr
for f, g, h 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 ) ) )

proof end;

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 ) )

proof end;

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

proof end;

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

proof end;

Lm5: for i being Nat
for R being non empty doubleLoopStr
for f, g being FinSequence of R st i <> 0 & i <= len g holds
(f ^ g) /. ((len f) + i) = g /. i

proof end;

definition
let R be non empty doubleLoopStr ;
let x be Scalar of R;
func x ^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;
attr x 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;
attr f is being_a_Sum_of_squares means :: 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 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;
attr x is being_a_sum_of_squares means :: 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 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

proof end;

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

proof end;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of R;
attr f is being_a_Product_of_squares means :: 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 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;
attr x is being_a_product_of_squares means :: 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 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

proof end;

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

proof end;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of R;
attr f is being_a_Sum_of_products_of_squares means :: 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 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;
attr x is being_a_sum_of_products_of_squares means :: 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 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

by Lm14;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of R;
attr f is being_an_Amalgam_of_squares means :: 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 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;
attr x is being_an_amalgam_of_squares means :: 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 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

proof end;

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

proof end;

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

proof end;

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

proof end;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of R;
attr f is being_a_Sum_of_amalgams_of_squares means :: 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 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;
attr x is being_a_sum_of_amalgams_of_squares means :: 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 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

proof end;

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

proof end;

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

proof end;

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

by Lm22;

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

proof end;

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

proof end;

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

proof end;

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

by Lm26;

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

proof end;

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

proof end;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of R;
attr f is being_a_generation_from_squares means :: 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 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;
attr x is generated_from_squares means :: 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 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

by Lm39;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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
proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;

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 ;

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 ;

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 ;

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 ;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;

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

proof end;

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 ;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;

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 ;

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 ;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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
proof end;

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
proof end;

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

proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;