let R be domRing; :: thesis: for S being domRingExtension of R
for p being non zero Element of the carrier of (Polynom-Ring R) holds card (Roots (S,p)) <= deg p
let S be domRingExtension of R; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring R) holds card (Roots (S,p)) <= deg p
let p be non zero Element of the carrier of (Polynom-Ring R); :: thesis: card (Roots (S,p)) <= deg p
the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring S) ;
p <> 0_. R ;
then q <> 0_. S by FIELD_4:12;
then reconsider q = q as non zero Element of the carrier of (Polynom-Ring S) by UPROOTS:def 5;
( Roots (S,p) = Roots q & deg p = deg q ) by FIELD_4:20, FIELD_7:13;
hence card (Roots (S,p)) <= deg p by RING_5:22; :: thesis: verum