:: O_RING_3 semantic presentation

Lm1: for n being Nat st n < 1 holds
n = 0

proof end;

Lm2: for n being Nat st n <> 0 holds
1 <= n

proof end;

Lm3: for n being Nat holds
( not n <= 1 or n = 0 or n = 1 )

proof end;

Lm4: for R being non empty doubleLoopStr
for h, f, g being FinSequence of the carrier 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;

Lm5: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R holds
( f = <*x*> iff ( len f = 1 & f .: 1 = x ) )

proof end;

Lm6: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R holds (f ^ <*x*>) .: ((len f) + 1) = x

proof end;

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

proof end;

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

proof end;

Lm9: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
<*x*> is_a_Product_of_squares

proof end;

Lm10: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
x is_a_product_of_squares

proof end;

Lm11: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
<*x*> is_an_Amalgam_of_squares

proof end;

Lm12: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
x is_an_amalgam_of_squares

proof end;

Lm13: for R being non empty doubleLoopStr
for f, g being FinSequence of the carrier of R st f is_an_Amalgam_of_squares & g is_an_Amalgam_of_squares holds
f ^ g is_an_Amalgam_of_squares

proof end;

Lm14: for R being non empty doubleLoopStr
for f, g being FinSequence of the carrier of R st f is_a_generation_from_squares & g is_a_generation_from_squares holds
f ^ g is_a_generation_from_squares

proof end;

Lm15: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R st f is_a_generation_from_squares & x is_a_square holds
f ^ <*x*> is_a_generation_from_squares

proof end;

Lm16: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R st f is_a_generation_from_squares & x is_an_amalgam_of_squares holds
f ^ <*x*> is_a_generation_from_squares

proof end;

Lm17: for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f .: i) * (f .: j))*> is_an_Amalgam_of_squares

proof end;

Lm18: for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f .: i) * (f .: j))*> is_a_generation_from_squares

proof end;

Lm19: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R st f is_a_Product_of_squares & x is_a_square holds
f ^ <*((f .: (len f)) * x)*> is_a_Product_of_squares

proof end;

Lm20: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R st f is_a_generation_from_squares & x is_a_square holds
(f ^ <*x*>) ^ <*((f .: (len f)) * x)*> is_a_generation_from_squares

proof end;

Lm21: for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of the carrier of R st f is_a_generation_from_squares & x is_an_amalgam_of_squares holds
(f ^ <*x*>) ^ <*((f .: (len f)) * x)*> is_a_generation_from_squares

proof end;

Lm22: for R being non empty doubleLoopStr
for f, g being FinSequence of the carrier of R st f is_an_Amalgam_of_squares & g is_an_Amalgam_of_squares holds
(f ^ g) ^ <*((f .: (len f)) * (g .: (len g)))*> is_an_Amalgam_of_squares

proof end;

Lm23: for R being non empty doubleLoopStr
for f, g being FinSequence of the carrier of R st f is_a_generation_from_squares & g is_a_generation_from_squares holds
(f ^ g) ^ <*((f .: (len f)) * (g .: (len g)))*> is_a_generation_from_squares

proof end;

theorem :: O_RING_3:1

for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_a_square holds
x * y is_a_product_of_squares

proof end;

theorem :: O_RING_3:2

for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_a_square holds
x * y is_a_product_of_squares

proof end;

Lm24: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_a_product_of_squares holds
x * y is_an_amalgam_of_squares

proof end;

Lm25: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_an_amalgam_of_squares holds
x * y is_an_amalgam_of_squares

proof end;

theorem :: O_RING_3:3

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_a_square & y is_a_product_of_squares ) or ( x is_a_square & y is_an_amalgam_of_squares ) ) holds
x * y is_an_amalgam_of_squares by Lm24, Lm25;

Lm26: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_a_product_of_squares holds
x * y is_an_amalgam_of_squares

proof end;

Lm27: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_an_amalgam_of_squares holds
x * y is_an_amalgam_of_squares

proof end;

theorem :: O_RING_3:4

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_a_product_of_squares & y is_a_product_of_squares ) or ( x is_a_product_of_squares & y is_an_amalgam_of_squares ) ) holds
x * y is_an_amalgam_of_squares by Lm26, Lm27;

Lm28: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_a_square holds
x * y is_an_amalgam_of_squares

proof end;

Lm29: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_a_product_of_squares holds
x * y is_an_amalgam_of_squares

proof end;

Lm30: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_an_amalgam_of_squares holds
x * y is_an_amalgam_of_squares

proof end;

theorem :: O_RING_3:5

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_an_amalgam_of_squares & y is_a_square ) or ( x is_an_amalgam_of_squares & y is_a_product_of_squares ) or ( x is_an_amalgam_of_squares & y is_an_amalgam_of_squares ) ) holds
x * y is_an_amalgam_of_squares by Lm28, Lm29, Lm30;

Lm31: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm32: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm33: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

Lm34: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_square & y is_generated_from_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:6

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_a_square & y is_a_sum_of_squares ) or ( x is_a_square & y is_a_sum_of_products_of_squares ) or ( x is_a_square & y is_a_sum_of_amalgams_of_squares ) or ( x is_a_square & y is_generated_from_squares ) ) holds
x * y is_generated_from_squares by Lm31, Lm32, Lm33, Lm34;

Lm35: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_a_square holds
x * y is_generated_from_squares

proof end;

Lm36: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm37: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_a_product_of_squares holds
x * y is_generated_from_squares

proof end;

Lm38: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm39: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_an_amalgam_of_squares holds
x * y is_generated_from_squares

proof end;

Lm40: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

Lm41: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_squares & y is_generated_from_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:7

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_a_sum_of_squares & y is_a_square ) or ( x is_a_sum_of_squares & y is_a_sum_of_squares ) or ( x is_a_sum_of_squares & y is_a_product_of_squares ) or ( x is_a_sum_of_squares & y is_a_sum_of_products_of_squares ) or ( x is_a_sum_of_squares & y is_an_amalgam_of_squares ) or ( x is_a_sum_of_squares & y is_a_sum_of_amalgams_of_squares ) or ( x is_a_sum_of_squares & y is_generated_from_squares ) ) holds
x * y is_generated_from_squares by Lm35, Lm36, Lm37, Lm38, Lm39, Lm40, Lm41;

Lm42: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm43: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm44: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

Lm45: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_product_of_squares & y is_generated_from_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:8

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_a_product_of_squares & y is_a_sum_of_squares ) or ( x is_a_product_of_squares & y is_a_sum_of_products_of_squares ) or ( x is_a_product_of_squares & y is_a_sum_of_amalgams_of_squares ) or ( x is_a_product_of_squares & y is_generated_from_squares ) ) holds
x * y is_generated_from_squares by Lm42, Lm43, Lm44, Lm45;

Lm46: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_a_square holds
x * y is_generated_from_squares

proof end;

Lm47: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm48: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_a_product_of_squares holds
x * y is_generated_from_squares

proof end;

Lm49: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm50: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_an_amalgam_of_squares holds
x * y is_generated_from_squares

proof end;

Lm51: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

Lm52: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_products_of_squares & y is_generated_from_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:9

Lm53: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm54: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm55: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

Lm56: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_an_amalgam_of_squares & y is_generated_from_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:10

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_an_amalgam_of_squares & y is_a_sum_of_squares ) or ( x is_an_amalgam_of_squares & y is_a_sum_of_products_of_squares ) or ( x is_an_amalgam_of_squares & y is_a_sum_of_amalgams_of_squares ) or ( x is_an_amalgam_of_squares & y is_generated_from_squares ) ) holds
x * y is_generated_from_squares by Lm53, Lm54, Lm55, Lm56;

Lm57: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_a_square holds
x * y is_generated_from_squares

proof end;

Lm58: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm59: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_a_product_of_squares holds
x * y is_generated_from_squares

proof end;

Lm60: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm61: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_an_amalgam_of_squares holds
x * y is_generated_from_squares

proof end;

Lm62: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

Lm63: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_a_sum_of_amalgams_of_squares & y is_generated_from_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:11

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is_a_sum_of_amalgams_of_squares & y is_a_square ) or ( x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_squares ) or ( x is_a_sum_of_amalgams_of_squares & y is_a_product_of_squares ) or ( x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_products_of_squares ) or ( x is_a_sum_of_amalgams_of_squares & y is_an_amalgam_of_squares ) or ( x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_amalgams_of_squares ) or ( x is_a_sum_of_amalgams_of_squares & y is_generated_from_squares ) ) holds
x * y is_generated_from_squares by Lm57, Lm58, Lm59, Lm60, Lm61, Lm62, Lm63;

Lm64: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_generated_from_squares & y is_a_square holds
x * y is_generated_from_squares

proof end;

Lm65: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_generated_from_squares & y is_an_amalgam_of_squares holds
x * y is_generated_from_squares

proof end;

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

Lm67: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_generated_from_squares & y is_a_sum_of_squares holds
x * y is_generated_from_squares

proof end;

Lm68: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_generated_from_squares & y is_a_product_of_squares holds
x * y is_generated_from_squares

proof end;

Lm69: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_generated_from_squares & y is_a_sum_of_products_of_squares holds
x * y is_generated_from_squares

proof end;

Lm70: for R being non empty doubleLoopStr
for x, y being Scalar of R st x is_generated_from_squares & y is_a_sum_of_amalgams_of_squares holds
x * y is_generated_from_squares

proof end;

theorem :: O_RING_3:12