consider a being Element of NonZero R;
reconsider a = a as Element of R ;
take q = a | (n,R); :: thesis: q is non-zero
A1: ( a <> 0. R & 0_ (n,R) = (0. R) | (n,R) ) by POLYNOM7:19, ZFMISC_1:64;
assume q = 0_ (n,R) ; :: according to POLYNOM7:def 2 :: thesis: contradiction
hence contradiction by A1, POLYNOM7:21; :: thesis: verum