:: deftheorem defines is_a_factorization_of RING_2:def 11 :
for R being non empty right_unital doubleLoopStr
for x being Element of R
for F being non empty FinSequence of R holds
( F is_a_factorization_of x iff ( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) ) );