let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; :: thesis: for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z
let z be non zero irreducible rational_function of L; :: thesis: NF z = NormRationalFunction z
consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF 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) ) ) ) ) by Def17;
consider f being FinSequence of (Polynom-Ring L) such that
A2: ( z2 = Product f & z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & ( 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) ) ) ) by A1;

now :: thesis: ( f <> <*> the carrier of (Polynom-Ring L) implies for i being Element of dom f holds contradiction )

assume A3: f <> <*> the carrier of (Polynom-Ring L) ; :: thesis: for i being Element of dom f holds contradiction
let i be Element of dom f; :: thesis: contradiction
dom f <> {} by A3;
then i in dom f ;
then reconsider i = i as Element of NAT ;
consider x being Element of L such that
A4: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by A2, A3;
z `1 ,z `2 have_common_roots by A4;
hence contradiction by Def10; :: thesis: verum

end;

then A5: Product f = 1_ (Polynom-Ring L) by GROUP_4:8
.= 1_. L by POLYNOM3:def 10 ;
then z = [(z1 `1),(z2 *' (z1 `2))] by A2, POLYNOM3:35
.= [(z1 `1),(z1 `2)] by A2, A5, POLYNOM3:35
.= z1 by Th19 ;
hence NF z = NormRationalFunction z by A1; :: thesis: verum