:: deftheorem Def17 defines NF RATFUNC1:def 17 :
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, b₃ being rational_function of L holds
( ( not z is zero implies ( b₃ = NF z iff ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b₃ = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) ) & ( z is zero implies ( b₃ = NF z iff b₃ = 0._ L ) ) );