p <> 0_. R ;
then A: p <> 0_. S by FIELD_4:12;
the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S) by FIELD_4:10;
then reconsider p1 = p as non zero Element of the carrier of (Polynom-Ring S) by A, UPROOTS:def 5;
Roots (S,p) = Roots p1 by m4;
hence Roots (S,p) is finite ; :: thesis: verum