set P = Polynom-Ring p;
1. (Polynom-Ring p) = 1_. F by defprfp;
hence 0. (Polynom-Ring p) <> 1. (Polynom-Ring p) by defprfp; :: according to STRUCT_0:def 8 :: thesis: verum