:: O_RING_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

definition
let D be non empty set ;
let f be FinSequence of D;
let k be Nat;
assume A1: ( 0 <> k & k <= len f ) ;
func f .: k -> Element of D equals :Def1: :: O_RING_1:def 1
f . k;
coherence
f . k is Element of D
proof end;
end;

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

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

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

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*>) .: ((len f) + 1) = x
proof end;

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

definition
let R be non empty doubleLoopStr ;
let x be Scalar of R;
func x ^2 -> Scalar of R equals :: O_RING_1:def 2
x * x;
coherence
x * x is Scalar of R ;
end;

:: deftheorem defines ^2 O_RING_1:def 2 :
for R being non empty doubleLoopStr
for x being Scalar of R holds x ^2 = x * x;

definition
let R be non empty doubleLoopStr ;
let x be Scalar of R;
attr x is being_a_square means :: O_RING_1:def 3
 ex y being Scalar of R st x = y ^2 ;
end;

:: deftheorem defines being_a_square O_RING_1:def 3 :
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 );

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_a_square for being_a_square x;
end;

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

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

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

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

:: deftheorem Def5 defines being_a_sum_of_squares O_RING_1:def 5 :
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 the carrier of R st
( f is_a_Sum_of_squares & x = f .: (len f) ) );

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_a_sum_of_squares for being_a_sum_of_squares x;
end;

Lm7: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
<*x*> is_a_Sum_of_squares
proof end;

Lm8: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
x is_a_sum_of_squares
proof end;

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

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

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

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

:: deftheorem Def7 defines being_a_product_of_squares O_RING_1:def 7 :
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 the carrier of R st
( f is_a_Product_of_squares & x = f .: (len f) ) );

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_a_product_of_squares for being_a_product_of_squares x;
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;

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

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

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

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

:: deftheorem Def9 defines being_a_sum_of_products_of_squares O_RING_1:def 9 :
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 the carrier of R st
( f is_a_Sum_of_products_of_squares & x = f .: (len f) ) );

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_a_sum_of_products_of_squares for being_a_sum_of_products_of_squares x;
end;

Lm11: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
<*x*> is_a_Sum_of_products_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_a_sum_of_products_of_squares
proof end;

Lm13: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
<*x*> is_a_Sum_of_products_of_squares
proof end;

Lm14: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
x is_a_sum_of_products_of_squares
proof end;

Lm15: for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_Sum_of_squares holds
f is_a_Sum_of_products_of_squares
proof end;

Lm16: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_squares holds
x is_a_sum_of_products_of_squares
proof end;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of the carrier of R;
attr f is being_an_Amalgam_of_squares means :Def10: :: O_RING_1:def 10
( len f <> 0 & ( for n being Nat st n <> 0 & n <= len f & not f .: n is_a_product_of_squares holds
ex i, j being Nat st
( f .: n = (f .: i) * (f .: j) & i <> 0 & i < n & j <> 0 & j < n ) ) );
end;

:: deftheorem Def10 defines being_an_Amalgam_of_squares O_RING_1:def 10 :
for R being non empty doubleLoopStr
for f being FinSequence of the carrier 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_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 ) ) ) );

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

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

:: deftheorem Def11 defines being_an_amalgam_of_squares O_RING_1:def 11 :
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 the carrier of R st
( f is_an_Amalgam_of_squares & x = f .: (len f) ) );

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_an_amalgam_of_squares for being_an_amalgam_of_squares x;
end;

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

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

Lm19: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
<*x*> is_an_Amalgam_of_squares
proof end;

Lm20: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
x is_an_amalgam_of_squares
proof end;

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

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

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

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

:: deftheorem Def13 defines being_a_sum_of_amalgams_of_squares O_RING_1:def 13 :
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 the carrier of R st
( f is_a_Sum_of_amalgams_of_squares & x = f .: (len f) ) );

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_a_sum_of_amalgams_of_squares for being_a_sum_of_amalgams_of_squares x;
end;

Lm21: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
<*x*> is_a_Sum_of_amalgams_of_squares
proof end;

Lm22: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
x is_a_sum_of_amalgams_of_squares
proof end;

Lm23: for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_Sum_of_squares holds
f is_a_Sum_of_amalgams_of_squares
proof end;

Lm24: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_squares holds
x is_a_sum_of_amalgams_of_squares
proof end;

Lm25: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
<*x*> is_a_Sum_of_amalgams_of_squares
proof end;

Lm26: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
x is_a_sum_of_amalgams_of_squares
proof end;

Lm27: for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_Sum_of_products_of_squares holds
f is_a_Sum_of_amalgams_of_squares
proof end;

Lm28: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_products_of_squares holds
x is_a_sum_of_amalgams_of_squares
proof end;

Lm29: for R being non empty doubleLoopStr
for x being Scalar of R st x is_an_amalgam_of_squares holds
<*x*> is_a_Sum_of_amalgams_of_squares
proof end;

Lm30: for R being non empty doubleLoopStr
for x being Scalar of R st x is_an_amalgam_of_squares holds
x is_a_sum_of_amalgams_of_squares
proof end;

definition
let R be non empty doubleLoopStr ;
let f be FinSequence of the carrier of R;
attr f is being_a_generation_from_squares means :Def14: :: O_RING_1:def 14
( len f <> 0 & ( for n being Nat st n <> 0 & n <= len f & not f .: n is_an_amalgam_of_squares holds
ex i, j being Nat st
( ( f .: n = (f .: i) * (f .: j) or f .: n = (f .: i) + (f .: j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) );
end;

:: deftheorem Def14 defines being_a_generation_from_squares O_RING_1:def 14 :
for R being non empty doubleLoopStr
for f being FinSequence of the carrier 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_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 ) ) ) );

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

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

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

notation
let R be non empty doubleLoopStr ;
let x be Scalar of R;
synonym x is_generated_from_squares for generated_from_squares x;
end;

Lm31: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
<*x*> is_a_generation_from_squares
proof end;

Lm32: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
x is_generated_from_squares
proof end;

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

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

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

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

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

Lm38: for i being Nat
for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_Sum_of_squares & 0 <> i & i <= len f holds
f .: i is_generated_from_squares
proof end;

Lm39: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_squares holds
x is_generated_from_squares
proof end;

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

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

Lm42: for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_an_Amalgam_of_squares holds
f is_a_generation_from_squares
proof end;

Lm43: for R being non empty doubleLoopStr
for x being Scalar of R st x is_an_amalgam_of_squares holds
x is_generated_from_squares
proof end;

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

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

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

Lm47: for i being Nat
for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_Product_of_squares & 0 <> i & i <= len f holds
f .: i is_generated_from_squares
proof end;

Lm48: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
x is_generated_from_squares
proof end;

Lm49: 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_product_of_squares holds
f ^ <*x*> is_a_generation_from_squares
proof end;

Lm50: 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_product_of_squares holds
(f ^ <*x*>) ^ <*((f .: (len f)) + x)*> is_a_generation_from_squares
proof end;

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

Lm52: for i being Nat
for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_a_Sum_of_products_of_squares & 0 <> i & i <= len f holds
f .: i is_generated_from_squares
proof end;

Lm53: for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_products_of_squares holds
x is_generated_from_squares
proof end;

theorem :: O_RING_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_square holds
( x is_a_sum_of_squares & x is_a_product_of_squares & x is_a_sum_of_products_of_squares & x is_an_amalgam_of_squares & x is_a_sum_of_amalgams_of_squares & x is_generated_from_squares ) by Lm8, Lm10, Lm12, Lm18, Lm22, Lm32;

theorem :: O_RING_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_squares holds
( x is_a_sum_of_products_of_squares & x is_a_sum_of_amalgams_of_squares & x is_generated_from_squares ) by Lm16, Lm24, Lm39;

theorem :: O_RING_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_product_of_squares holds
( x is_a_sum_of_products_of_squares & x is_an_amalgam_of_squares & x is_a_sum_of_amalgams_of_squares & x is_generated_from_squares ) by Lm14, Lm20, Lm26, Lm48;

theorem :: O_RING_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_products_of_squares holds
( x is_a_sum_of_amalgams_of_squares & x is_generated_from_squares ) by Lm28, Lm53;

theorem :: O_RING_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for x being Scalar of R st x is_an_amalgam_of_squares holds
( x is_a_sum_of_amalgams_of_squares & x is_generated_from_squares ) by Lm30, Lm43;

Lm54: for R being non empty doubleLoopStr
for f being FinSequence of the carrier of R st f is_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 :: O_RING_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr
for x being Scalar of R st x is_a_sum_of_amalgams_of_squares holds
x is_generated_from_squares
proof end;