:: Ordered Rings - Part I
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received October 11, 1990
:: 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 Lm7, Lm9, Lm11, Lm17, Lm21, Lm31;

theorem :: O_RING_1:3

for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_squares holds
( x is being_a_sum_of_products_of_squares & x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares ) by Lm15, Lm23, Lm38;

theorem :: O_RING_1:4

for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
( x is being_a_sum_of_products_of_squares & x is being_an_amalgam_of_squares & x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares ) by Lm13, Lm19, Lm25, Lm49;

theorem :: O_RING_1:5

for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_products_of_squares holds
( x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares ) by Lm27, Lm54;

theorem :: O_RING_1:6

for R being non empty doubleLoopStr
for x being Scalar of R st x is being_an_amalgam_of_squares holds
( x is being_a_sum_of_amalgams_of_squares & x is generated_from_squares ) by Lm29, Lm40;

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 Lm56, Lm62;

Lm65: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_square holds
x + y is being_a_sum_of_products_of_squares

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 Lm58, Lm65;

Lm66: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_product_of_squares holds
x + y is being_a_sum_of_amalgams_of_squares

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 Lm60, Lm66, Lm67, Lm68, Lm69;

Lm70: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_squares holds
x + y is generated_from_squares

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 Lm40, Lm72;

Lm75: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_amalgams_of_squares holds
x + y is generated_from_squares
by Lm72, Th1;

theorem :: O_RING_1:10

for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & ( y is being_a_sum_of_squares or y is being_a_product_of_squares or y is being_a_sum_of_products_of_squares or y is being_an_amalgam_of_squares or y is being_a_sum_of_amalgams_of_squares or y is generated_from_squares ) holds
x + y is generated_from_squares by Lm70, Lm71, Lm72, Lm73, Lm74, Lm75;

theorem :: O_RING_1:11

for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_sum_of_squares holds
x + y is generated_from_squares

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 Lm36, Lm43, Lm64, Lm76, Lm77, Lm78, Lm79;

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;