:: deftheorem defines being_a_product_of_squares O_RING_1:def 6 :
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 R st
( f is being_a_Product_of_squares & x = f /. (len f) ) );