theorem Th2: :: POLYNOM8:2

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for x, y being Element of L st x <> 0. L & y <> 0. L holds
(x * y) " = (x ") * (y ")