:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba

::

:: Received October 11, 1990

:: Copyright (c) 1990-2016 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
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;

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

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;

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

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

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;

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

ex f being FinSequence of R st

( f is being_a_Sum_of_squares & x = f /. (len f) );

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

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;

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

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

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;

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

ex f being FinSequence of R st

( f is being_a_Product_of_squares & x = f /. (len f) );

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

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;

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

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

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;

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

ex f being FinSequence of R st

( f is being_a_Sum_of_products_of_squares & x = f /. (len f) );

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

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;

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

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;

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

ex f being FinSequence of R st

( f is being_an_Amalgam_of_squares & x = f /. (len f) );

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

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;

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

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

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;

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

ex f being FinSequence of R st

( f is being_a_Sum_of_amalgams_of_squares & x = f /. (len f) );

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

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;

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

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

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;

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

ex f being FinSequence of R st

( f is being_a_generation_from_squares & x = f /. (len f) );

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

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

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;

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;

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;

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;

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;

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;

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;

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;

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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;

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

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

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

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

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

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

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

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

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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;