O_RING

:: O_RING_1 semantic presentation

begin

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

func x ^2 -> ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) equals :: O_RING_1:def 1
x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) * x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) ;

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is being_a_square means :: O_RING_1:def 2
ex y being ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) st x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ^2 : ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) ;

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let f be ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ;

attr f is being_a_Sum_of_squares means :: O_RING_1:def 3
( len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) is being_a_square & ( for n being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) holds
ex y being ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) st
( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. (n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) + 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) ) ) );

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is being_a_sum_of_squares means :: O_RING_1:def 4
ex f being ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) is being_a_Sum_of_squares & x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) /. (len f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) );

end;

definition

attr f is being_a_Product_of_squares means :: O_RING_1:def 5
( len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) is being_a_square & ( for n being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) holds
ex y being ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) st
( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. (n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) + 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) ) ) );

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is being_a_product_of_squares means :: O_RING_1:def 6
ex f being ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) is being_a_Product_of_squares & x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) /. (len f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) );

end;

definition

attr f is being_a_Sum_of_products_of_squares means :: O_RING_1:def 7
( len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) is being_a_product_of_squares & ( for n being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) holds
ex y being ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) st
( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. (n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) + 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) ) ) );

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is being_a_sum_of_products_of_squares means :: O_RING_1:def 8
ex f being ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) is being_a_Sum_of_products_of_squares & x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) /. (len f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) );

end;

definition

attr f is being_an_Amalgam_of_squares means :: O_RING_1:def 9
( len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & ( for n being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <= len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & not f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) is being_a_product_of_squares holds
ex i, j being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st
( f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) * (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) & i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) & j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) ) );

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is being_an_amalgam_of_squares means :: O_RING_1:def 10
ex f being ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) is being_an_Amalgam_of_squares & x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) /. (len f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) );

end;

definition

attr f is being_a_Sum_of_amalgams_of_squares means :: O_RING_1:def 11
( len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) is being_an_amalgam_of_squares & ( for n being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) holds
ex y being ( ( ) ( ) Scalar of ( ( ) ( ) set ) ) st
( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. (n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) + 1 : ( ( ) ( V11() V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) ) ) );

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is being_a_sum_of_amalgams_of_squares means :: O_RING_1:def 12
ex f being ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) is being_a_Sum_of_amalgams_of_squares & x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) /. (len f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) );

end;

definition

attr f is being_a_generation_from_squares means :: O_RING_1:def 13
( len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & ( for n being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <= len f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & not f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) is being_an_amalgam_of_squares holds
ex i, j being ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) st
( ( f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) * (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) or f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) = (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) + (f : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) /. j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) ) & i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & i : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) & j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) <> 0 : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) & j : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) < n : ( ( V27() ) ( V21() V22() V23() V27() V28() ext-real V103() ) Nat) ) ) );

end;

definition

let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let x be ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) ;

attr x is generated_from_squares means :: O_RING_1:def 14
ex f being ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) is being_a_generation_from_squares & x : ( ( ) ( ) VectSpStr over R : ( ( ) ( ) L1()) ) = f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) /. (len f : ( ( ) ( V1() V4(K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) V5( the U1 of R : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) ) Function-like V29() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V21() V22() V23() V27() V28() ext-real V103() ) M3(K88() : ( ( ) ( ) set ) ,K92() : ( ( ) ( V11() V21() V22() V23() ) M2(K19(K88() : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( ) M2( the U1 of R : ( ( ) ( ) L1()) : ( ( ) ( ) set ) )) );

end;

theorem :: O_RING_1:1

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ;

theorem :: O_RING_1:2

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) ;

theorem :: O_RING_1:3

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) ;

theorem :: O_RING_1:4

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) ;

theorem :: O_RING_1:5

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) ;

theorem :: O_RING_1:6

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) ;

begin

theorem :: O_RING_1:7

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st ( ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square ) ) holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_a_sum_of_squares ;

theorem :: O_RING_1:8

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st ( ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares ) ) holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_a_sum_of_products_of_squares ;

theorem :: O_RING_1:9

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st ( ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & ( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares ) ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & ( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares ) ) ) holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_a_sum_of_amalgams_of_squares ;

theorem :: O_RING_1:10

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & ( y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares or y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:11

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:12

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:13

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:14

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:15

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:16

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:17

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:18

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:19

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:20

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:21

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:22

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:23

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:24

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:25

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:26

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:27

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:28

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:29

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:30

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:31

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:32

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:33

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:34

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:35

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:36

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:37

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:38

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st ( ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares ) or ( x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares ) ) holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

begin

theorem :: O_RING_1:39

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_a_product_of_squares ;

theorem :: O_RING_1:40

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_a_product_of_squares ;

theorem :: O_RING_1:41

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:42

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:43

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:44

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:45

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:46

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:47

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is being_an_amalgam_of_squares ;

theorem :: O_RING_1:48

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:49

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:50

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:51

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:52

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:53

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:54

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:55

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:56

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:57

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:58

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:59

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:60

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:61

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:62

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:63

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:64

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:65

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:66

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:67

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:68

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:69

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:70

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:71

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:72

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:73

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:74

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:75

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:76

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:77

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:78

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:79

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:80

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:81

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_square holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:82

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_an_amalgam_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:83

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:84

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_product_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:85

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_products_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;

theorem :: O_RING_1:86

for R being ( ( non empty ) ( non empty ) doubleLoopStr )
for x, y being ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) st x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is generated_from_squares & y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) is being_a_sum_of_amalgams_of_squares holds
x : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) M2( the U1 of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( V11() ) set ) )) is generated_from_squares ;