reconsider q = p as Polynomial of S by FIELD_4:8;
p <> 0_. R ;
then q <> 0_. S by FIELD_4:12;
then reconsider q = q as non zero Polynomial of S by UPROOTS:def 5;
take multiplicity (q,a) ; :: thesis: ex q being non zero Polynomial of S st
( q = p & multiplicity (q,a) = multiplicity (q,a) )
thus ex q being non zero Polynomial of S st
( q = p & multiplicity (q,a) = multiplicity (q,a) ) ; :: thesis: verum