theorem Th20: :: RATFUNC1:20

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p being rational_function of L
for a being non zero Element of L holds
( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )