:: deftheorem ddf defines Factorization RING_2:def 13 :
for R being non empty right_unital doubleLoopStr
for x being Element of R st x is factorizable holds
for b₃ being non empty FinSequence of R holds
( b₃ is Factorization of x iff b₃ is_a_factorization_of x );