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