let L be Field; :: thesis: for f being Polynomial of L st 0 <= deg f holds
( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) )
let f be Polynomial of L; :: thesis: ( 0 <= deg f implies ( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) ) )
assume A1: 0 <= deg f ; :: thesis: ( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) )
then reconsider n = deg f as Element of NAT by INT_1:3;
reconsider f = f as non-zero Polynomial of L by A1, Th26;
ex m being Element of NAT st
( m = card (Roots f) & m <= n ) by Lm13;
hence ( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) ) ; :: thesis: verum