:: O_RING_1 semantic presentation

Lemma1: for b1 being Nat st b1 < 1 holds
b1 = 0
proof end;

Lemma2: for b1 being Nat holds
( not b1 <= 1 or b1 = 0 or b1 = 1 )
proof end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be Nat;
assume E3: ( 0 <> c3 & c3 <= len c2 ) ;
func c2 .: c3 -> Element of a1 equals :Def1: :: O_RING_1:def 1
a2 . a3;
coherence
c2 . c3 is Element of c1
proof end;
end;

:: deftheorem Def1 defines .: O_RING_1:def 1 :
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Nat st 0 <> b3 & b3 <= len b2 holds
b2 .: b3 = b2 . b3;

Lemma4: for b1 being non empty doubleLoopStr
for b2, b3, b4 being FinSequence of the carrier of b1 holds
( b2 = b3 ^ b4 iff ( dom b2 = Seg ((len b3) + (len b4)) & ( for b5 being Nat st b5 in dom b3 holds
b2 .: b5 = b3 .: b5 ) & ( for b5 being Nat st b5 in dom b4 holds
b2 .: ((len b3) + b5) = b4 .: b5 ) ) )
proof end;

Lemma5: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 holds
( b3 = <*b2*> iff ( len b3 = 1 & b3 .: 1 = b2 ) )
proof end;

Lemma6: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 holds (b3 ^ <*b2*>) .: ((len b3) + 1) = b2
proof end;

Lemma7: for b1 being Nat
for b2 being non empty doubleLoopStr
for b3, b4 being FinSequence of the carrier of b2 st b1 <> 0 & b1 <= len b3 holds
(b3 ^ b4) .: b1 = b3 .: b1
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
func c2 ^2 -> Scalar of a1 equals :: O_RING_1:def 2
a2 * a2;
coherence
c2 * c2 is Scalar of c1 ;
end;

:: deftheorem Def2 defines ^2 O_RING_1:def 2 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds b2 ^2 = b2 * b2;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is being_a_square means :: O_RING_1:def 3
ex b1 being Scalar of a1 st a2 = b1 ^2 ;
end;

:: deftheorem Def3 defines being_a_square O_RING_1:def 3 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is being_a_square iff ex b3 being Scalar of b1 st b2 = b3 ^2 );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_a_square for being_a_square c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
attr a2 is being_a_Sum_of_squares means :Def4: :: O_RING_1:def 4
( len a2 <> 0 & a2 .: 1 is_a_square & ( for b1 being Nat st b1 <> 0 & b1 < len a2 holds
ex b2 being Scalar of a1 st
( b2 is_a_square & a2 .: (b1 + 1) = (a2 .: b1) + b2 ) ) );
end;

:: deftheorem Def4 defines being_a_Sum_of_squares O_RING_1:def 4 :
for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 holds
( b2 is being_a_Sum_of_squares iff ( len b2 <> 0 & b2 .: 1 is_a_square & ( for b3 being Nat st b3 <> 0 & b3 < len b2 holds
ex b4 being Scalar of b1 st
( b4 is_a_square & b2 .: (b3 + 1) = (b2 .: b3) + b4 ) ) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
synonym c2 is_a_Sum_of_squares for being_a_Sum_of_squares c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is being_a_sum_of_squares means :Def5: :: O_RING_1:def 5
ex b1 being FinSequence of the carrier of a1 st
( b1 is_a_Sum_of_squares & a2 = b1 .: (len b1) );
end;

:: deftheorem Def5 defines being_a_sum_of_squares O_RING_1:def 5 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is being_a_sum_of_squares iff ex b3 being FinSequence of the carrier of b1 st
( b3 is_a_Sum_of_squares & b2 = b3 .: (len b3) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_a_sum_of_squares for being_a_sum_of_squares c2;
end;

Lemma10: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
<*b2*> is_a_Sum_of_squares
proof end;

Lemma11: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
b2 is_a_sum_of_squares
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
attr a2 is being_a_Product_of_squares means :Def6: :: O_RING_1:def 6
( len a2 <> 0 & a2 .: 1 is_a_square & ( for b1 being Nat st b1 <> 0 & b1 < len a2 holds
ex b2 being Scalar of a1 st
( b2 is_a_square & a2 .: (b1 + 1) = (a2 .: b1) * b2 ) ) );
end;

:: deftheorem Def6 defines being_a_Product_of_squares O_RING_1:def 6 :
for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 holds
( b2 is being_a_Product_of_squares iff ( len b2 <> 0 & b2 .: 1 is_a_square & ( for b3 being Nat st b3 <> 0 & b3 < len b2 holds
ex b4 being Scalar of b1 st
( b4 is_a_square & b2 .: (b3 + 1) = (b2 .: b3) * b4 ) ) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
synonym c2 is_a_Product_of_squares for being_a_Product_of_squares c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is being_a_product_of_squares means :Def7: :: O_RING_1:def 7
ex b1 being FinSequence of the carrier of a1 st
( b1 is_a_Product_of_squares & a2 = b1 .: (len b1) );
end;

:: deftheorem Def7 defines being_a_product_of_squares O_RING_1:def 7 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is being_a_product_of_squares iff ex b3 being FinSequence of the carrier of b1 st
( b3 is_a_Product_of_squares & b2 = b3 .: (len b3) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_a_product_of_squares for being_a_product_of_squares c2;
end;

Lemma14: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
<*b2*> is_a_Product_of_squares
proof end;

Lemma15: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
b2 is_a_product_of_squares
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
attr a2 is being_a_Sum_of_products_of_squares means :Def8: :: O_RING_1:def 8
( len a2 <> 0 & a2 .: 1 is_a_product_of_squares & ( for b1 being Nat st b1 <> 0 & b1 < len a2 holds
ex b2 being Scalar of a1 st
( b2 is_a_product_of_squares & a2 .: (b1 + 1) = (a2 .: b1) + b2 ) ) );
end;

:: deftheorem Def8 defines being_a_Sum_of_products_of_squares O_RING_1:def 8 :
for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 holds
( b2 is being_a_Sum_of_products_of_squares iff ( len b2 <> 0 & b2 .: 1 is_a_product_of_squares & ( for b3 being Nat st b3 <> 0 & b3 < len b2 holds
ex b4 being Scalar of b1 st
( b4 is_a_product_of_squares & b2 .: (b3 + 1) = (b2 .: b3) + b4 ) ) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
synonym c2 is_a_Sum_of_products_of_squares for being_a_Sum_of_products_of_squares c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is being_a_sum_of_products_of_squares means :Def9: :: O_RING_1:def 9
ex b1 being FinSequence of the carrier of a1 st
( b1 is_a_Sum_of_products_of_squares & a2 = b1 .: (len b1) );
end;

:: deftheorem Def9 defines being_a_sum_of_products_of_squares O_RING_1:def 9 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is being_a_sum_of_products_of_squares iff ex b3 being FinSequence of the carrier of b1 st
( b3 is_a_Sum_of_products_of_squares & b2 = b3 .: (len b3) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_a_sum_of_products_of_squares for being_a_sum_of_products_of_squares c2;
end;

Lemma18: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
<*b2*> is_a_Sum_of_products_of_squares
proof end;

Lemma19: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
b2 is_a_sum_of_products_of_squares
proof end;

Lemma20: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
<*b2*> is_a_Sum_of_products_of_squares
proof end;

Lemma21: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
b2 is_a_sum_of_products_of_squares
proof end;

Lemma22: for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 st b2 is_a_Sum_of_squares holds
b2 is_a_Sum_of_products_of_squares
proof end;

Lemma23: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_squares holds
b2 is_a_sum_of_products_of_squares
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
attr a2 is being_an_Amalgam_of_squares means :Def10: :: O_RING_1:def 10
( len a2 <> 0 & ( for b1 being Nat st b1 <> 0 & b1 <= len a2 & not a2 .: b1 is_a_product_of_squares holds
ex b2, b3 being Nat st
( a2 .: b1 = (a2 .: b2) * (a2 .: b3) & b2 <> 0 & b2 < b1 & b3 <> 0 & b3 < b1 ) ) );
end;

:: deftheorem Def10 defines being_an_Amalgam_of_squares O_RING_1:def 10 :
for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 holds
( b2 is being_an_Amalgam_of_squares iff ( len b2 <> 0 & ( for b3 being Nat st b3 <> 0 & b3 <= len b2 & not b2 .: b3 is_a_product_of_squares holds
ex b4, b5 being Nat st
( b2 .: b3 = (b2 .: b4) * (b2 .: b5) & b4 <> 0 & b4 < b3 & b5 <> 0 & b5 < b3 ) ) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
synonym c2 is_an_Amalgam_of_squares for being_an_Amalgam_of_squares c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is being_an_amalgam_of_squares means :Def11: :: O_RING_1:def 11
ex b1 being FinSequence of the carrier of a1 st
( b1 is_an_Amalgam_of_squares & a2 = b1 .: (len b1) );
end;

:: deftheorem Def11 defines being_an_amalgam_of_squares O_RING_1:def 11 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is being_an_amalgam_of_squares iff ex b3 being FinSequence of the carrier of b1 st
( b3 is_an_Amalgam_of_squares & b2 = b3 .: (len b3) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_an_amalgam_of_squares for being_an_amalgam_of_squares c2;
end;

Lemma26: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
<*b2*> is_an_Amalgam_of_squares
proof end;

Lemma27: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
b2 is_an_amalgam_of_squares
proof end;

Lemma28: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
<*b2*> is_an_Amalgam_of_squares
proof end;

Lemma29: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
b2 is_an_amalgam_of_squares
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
attr a2 is being_a_Sum_of_amalgams_of_squares means :Def12: :: O_RING_1:def 12
( len a2 <> 0 & a2 .: 1 is_an_amalgam_of_squares & ( for b1 being Nat st b1 <> 0 & b1 < len a2 holds
ex b2 being Scalar of a1 st
( b2 is_an_amalgam_of_squares & a2 .: (b1 + 1) = (a2 .: b1) + b2 ) ) );
end;

:: deftheorem Def12 defines being_a_Sum_of_amalgams_of_squares O_RING_1:def 12 :
for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 holds
( b2 is being_a_Sum_of_amalgams_of_squares iff ( len b2 <> 0 & b2 .: 1 is_an_amalgam_of_squares & ( for b3 being Nat st b3 <> 0 & b3 < len b2 holds
ex b4 being Scalar of b1 st
( b4 is_an_amalgam_of_squares & b2 .: (b3 + 1) = (b2 .: b3) + b4 ) ) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
synonym c2 is_a_Sum_of_amalgams_of_squares for being_a_Sum_of_amalgams_of_squares c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is being_a_sum_of_amalgams_of_squares means :Def13: :: O_RING_1:def 13
ex b1 being FinSequence of the carrier of a1 st
( b1 is_a_Sum_of_amalgams_of_squares & a2 = b1 .: (len b1) );
end;

:: deftheorem Def13 defines being_a_sum_of_amalgams_of_squares O_RING_1:def 13 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is being_a_sum_of_amalgams_of_squares iff ex b3 being FinSequence of the carrier of b1 st
( b3 is_a_Sum_of_amalgams_of_squares & b2 = b3 .: (len b3) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_a_sum_of_amalgams_of_squares for being_a_sum_of_amalgams_of_squares c2;
end;

Lemma32: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
<*b2*> is_a_Sum_of_amalgams_of_squares
proof end;

Lemma33: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
b2 is_a_sum_of_amalgams_of_squares
proof end;

Lemma34: for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 st b2 is_a_Sum_of_squares holds
b2 is_a_Sum_of_amalgams_of_squares
proof end;

Lemma35: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_squares holds
b2 is_a_sum_of_amalgams_of_squares
proof end;

Lemma36: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
<*b2*> is_a_Sum_of_amalgams_of_squares
proof end;

Lemma37: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
b2 is_a_sum_of_amalgams_of_squares
proof end;

Lemma38: for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 st b2 is_a_Sum_of_products_of_squares holds
b2 is_a_Sum_of_amalgams_of_squares
proof end;

Lemma39: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_products_of_squares holds
b2 is_a_sum_of_amalgams_of_squares
proof end;

Lemma40: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_an_amalgam_of_squares holds
<*b2*> is_a_Sum_of_amalgams_of_squares
proof end;

Lemma41: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_an_amalgam_of_squares holds
b2 is_a_sum_of_amalgams_of_squares
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
attr a2 is being_a_generation_from_squares means :Def14: :: O_RING_1:def 14
( len a2 <> 0 & ( for b1 being Nat st b1 <> 0 & b1 <= len a2 & not a2 .: b1 is_an_amalgam_of_squares holds
ex b2, b3 being Nat st
( ( a2 .: b1 = (a2 .: b2) * (a2 .: b3) or a2 .: b1 = (a2 .: b2) + (a2 .: b3) ) & b2 <> 0 & b2 < b1 & b3 <> 0 & b3 < b1 ) ) );
end;

:: deftheorem Def14 defines being_a_generation_from_squares O_RING_1:def 14 :
for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 holds
( b2 is being_a_generation_from_squares iff ( len b2 <> 0 & ( for b3 being Nat st b3 <> 0 & b3 <= len b2 & not b2 .: b3 is_an_amalgam_of_squares holds
ex b4, b5 being Nat st
( ( b2 .: b3 = (b2 .: b4) * (b2 .: b5) or b2 .: b3 = (b2 .: b4) + (b2 .: b5) ) & b4 <> 0 & b4 < b3 & b5 <> 0 & b5 < b3 ) ) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be FinSequence of the carrier of c1;
synonym c2 is_a_generation_from_squares for being_a_generation_from_squares c2;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
attr a2 is generated_from_squares means :Def15: :: O_RING_1:def 15
ex b1 being FinSequence of the carrier of a1 st
( b1 is_a_generation_from_squares & a2 = b1 .: (len b1) );
end;

:: deftheorem Def15 defines generated_from_squares O_RING_1:def 15 :
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 holds
( b2 is generated_from_squares iff ex b3 being FinSequence of the carrier of b1 st
( b3 is_a_generation_from_squares & b2 = b3 .: (len b3) ) );

notation
let c1 be non empty doubleLoopStr ;
let c2 be Scalar of c1;
synonym c2 is_generated_from_squares for generated_from_squares c2;
end;

Lemma44: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
<*b2*> is_a_generation_from_squares
proof end;

Lemma45: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
b2 is_generated_from_squares
proof end;

Lemma46: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_an_amalgam_of_squares holds
b3 ^ <*b2*> is_a_generation_from_squares
proof end;

Lemma47: for b1, b2 being Nat
for b3 being non empty doubleLoopStr
for b4 being FinSequence of the carrier of b3 st b4 is_a_generation_from_squares & b1 <> 0 & b1 <= len b4 & b2 <> 0 & b2 <= len b4 holds
b4 ^ <*((b4 .: b1) + (b4 .: b2))*> is_a_generation_from_squares
proof end;

Lemma48: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_a_square holds
b3 ^ <*b2*> is_a_generation_from_squares
proof end;

Lemma49: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_a_square holds
(b3 ^ <*b2*>) ^ <*((b3 .: (len b3)) + b2)*> is_a_generation_from_squares
proof end;

Lemma50: for b1 being non empty doubleLoopStr
for b2, b3 being Scalar of b1 st b2 is_generated_from_squares & b3 is_a_square holds
b2 + b3 is_generated_from_squares
proof end;

Lemma51: for b1 being Nat
for b2 being non empty doubleLoopStr
for b3 being FinSequence of the carrier of b2 st b3 is_a_Sum_of_squares & 0 <> b1 & b1 <= len b3 holds
b3 .: b1 is_generated_from_squares
proof end;

Lemma52: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_squares holds
b2 is_generated_from_squares
proof end;

Lemma53: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_an_amalgam_of_squares holds
(b3 ^ <*b2*>) ^ <*((b3 .: (len b3)) + b2)*> is_a_generation_from_squares
proof end;

Lemma54: for b1 being non empty doubleLoopStr
for b2, b3 being Scalar of b1 st b2 is_generated_from_squares & b3 is_an_amalgam_of_squares holds
b2 + b3 is_generated_from_squares
proof end;

Lemma55: for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 st b2 is_an_Amalgam_of_squares holds
b2 is_a_generation_from_squares
proof end;

Lemma56: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_an_amalgam_of_squares holds
b2 is_generated_from_squares
proof end;

Lemma57: for b1, b2 being Nat
for b3 being non empty doubleLoopStr
for b4 being FinSequence of the carrier of b3 st b4 is_a_generation_from_squares & b1 <> 0 & b1 <= len b4 & b2 <> 0 & b2 <= len b4 holds
b4 ^ <*((b4 .: b1) * (b4 .: b2))*> is_a_generation_from_squares
proof end;

Lemma58: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_a_square holds
(b3 ^ <*b2*>) ^ <*((b3 .: (len b3)) * b2)*> is_a_generation_from_squares
proof end;

Lemma59: for b1 being non empty doubleLoopStr
for b2, b3 being Scalar of b1 st b2 is_generated_from_squares & b3 is_a_square holds
b2 * b3 is_generated_from_squares
proof end;

Lemma60: for b1 being Nat
for b2 being non empty doubleLoopStr
for b3 being FinSequence of the carrier of b2 st b3 is_a_Product_of_squares & 0 <> b1 & b1 <= len b3 holds
b3 .: b1 is_generated_from_squares
proof end;

Lemma61: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
b2 is_generated_from_squares
proof end;

Lemma62: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_a_product_of_squares holds
b3 ^ <*b2*> is_a_generation_from_squares
proof end;

Lemma63: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1
for b3 being FinSequence of the carrier of b1 st b3 is_a_generation_from_squares & b2 is_a_product_of_squares holds
(b3 ^ <*b2*>) ^ <*((b3 .: (len b3)) + b2)*> is_a_generation_from_squares
proof end;

Lemma64: for b1 being non empty doubleLoopStr
for b2, b3 being Scalar of b1 st b2 is_generated_from_squares & b3 is_a_product_of_squares holds
b2 + b3 is_generated_from_squares
proof end;

Lemma65: for b1 being Nat
for b2 being non empty doubleLoopStr
for b3 being FinSequence of the carrier of b2 st b3 is_a_Sum_of_products_of_squares & 0 <> b1 & b1 <= len b3 holds
b3 .: b1 is_generated_from_squares
proof end;

Lemma66: for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_products_of_squares holds
b2 is_generated_from_squares
proof end;

theorem Th1: :: O_RING_1:1
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_square holds
( b2 is_a_sum_of_squares & b2 is_a_product_of_squares & b2 is_a_sum_of_products_of_squares & b2 is_an_amalgam_of_squares & b2 is_a_sum_of_amalgams_of_squares & b2 is_generated_from_squares ) by Lemma11, Lemma15, Lemma19, Lemma27, Lemma33, Lemma45;

theorem Th2: :: O_RING_1:2
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_squares holds
( b2 is_a_sum_of_products_of_squares & b2 is_a_sum_of_amalgams_of_squares & b2 is_generated_from_squares ) by Lemma23, Lemma35, Lemma52;

theorem Th3: :: O_RING_1:3
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_product_of_squares holds
( b2 is_a_sum_of_products_of_squares & b2 is_an_amalgam_of_squares & b2 is_a_sum_of_amalgams_of_squares & b2 is_generated_from_squares ) by Lemma21, Lemma29, Lemma37, Lemma61;

theorem Th4: :: O_RING_1:4
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_products_of_squares holds
( b2 is_a_sum_of_amalgams_of_squares & b2 is_generated_from_squares ) by Lemma39, Lemma66;

theorem Th5: :: O_RING_1:5
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_an_amalgam_of_squares holds
( b2 is_a_sum_of_amalgams_of_squares & b2 is_generated_from_squares ) by Lemma41, Lemma56;

Lemma67: for b1 being non empty doubleLoopStr
for b2 being FinSequence of the carrier of b1 st b2 is_a_Sum_of_amalgams_of_squares holds
for b3 being Nat st b3 <> 0 & b3 <= len b2 holds
b2 .: b3 is_generated_from_squares
proof end;

theorem Th6: :: O_RING_1:6
for b1 being non empty doubleLoopStr
for b2 being Scalar of b1 st b2 is_a_sum_of_amalgams_of_squares holds
b2 is_generated_from_squares
proof end;