:: deftheorem defines uniquely_factorizable RING_2:def 14 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is uniquely_factorizable iff ( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) ) );