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