for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being non zero rational_function of L holds
( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )