:: deftheorem defines being_an_Amalgam_of_squares O_RING_1:def 9 :
for R being non empty doubleLoopStr
for f being FinSequence 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 being_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 ) ) ) );