theorem :: RATFUNC1:25

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z by Lm4;