:: deftheorem defines factorizable RING_2:def 12 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is factorizable iff ex F being non empty FinSequence of R st F is_a_factorization_of x );