theorem fact2: :: RING_2:28

for R being non empty well-unital associative doubleLoopStr
for a, b being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds
F ^ G is_a_factorization_of a * b