:: deftheorem defines being_an_amalgam_of_squares O_RING_1:def 10 :
for R being non empty doubleLoopStr
for x being Scalar of R holds
( x is being_an_amalgam_of_squares iff ex f being FinSequence of R st
( f is being_an_Amalgam_of_squares & x = f /. (len f) ) );