z `1 <> 0_. L by Def9;
then reconsider z1 = z `1 as non zero Polynomial of L by UPROOTS:def 5;
not ((1. L) / (LC (z `2))) * z1 is zero ;
then (NormRatF z) `1 <> 0_. L ;
hence not NormRationalFunction z is zero ; :: thesis: verum