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