set a = the Element of NonZero R;
reconsider a = the Element of NonZero R 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:56;
assume q = 0_ (n,R) ; :: according to POLYNOM7:def 1 :: thesis: contradiction
hence contradiction by A1, POLYNOM7:21; :: thesis: verum