consider a being Element of the carrier of R \ {(0. R)};
A1: not the carrier of R \ {(0. R)} is zero by REALSET1:4;
then A2: ( a in the carrier of R & not a in {(0. R)} ) by XBOOLE_0:def 5;
reconsider a = a as Element of R by A1, XBOOLE_0:def 5;
set q = a | n,R;
A3: a <> 0. R by A2, TARSKI:def 1;
take a | n,R ; :: thesis: a | n,R is non-zero

now

assume A4: a | n,R = 0_ n,R ; :: thesis: contradiction
0_ n,R = (0. R) | n,R by POLYNOM7:19;
hence contradiction by A3, A4, POLYNOM7:21; :: thesis: verum

end;

hence a | n,R is non-zero by POLYNOM7:def 2; :: thesis: verum