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