consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
H: ( 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 defNF;

now :: thesis: not z1 `1 = 0_. L

assume z1 `1 = 0_. L ; :: thesis: contradiction
then 0_. L = z2 *' (z1 `1) by POLYNOM3:34
.= z `1 by H, XTUPLE_0:def 2 ;
hence contradiction by defzerrat; :: thesis: verum

end;

then not z1 is zero by defzerrat;
hence not NF z is zero by H; :: thesis: verum