let R be domRing; :: thesis: for p being non zero Polynomial of R ex n being natural number st
( n = card () & n <= deg p )

let p be non zero Polynomial of R; :: thesis: ex n being natural number st
( n = card () & n <= deg p )

defpred S1[ Nat] means for p being non zero Polynomial of R st deg p = \$1 holds
ex n being natural number st
( n = card () & n <= deg p );
IA: S1[ 0 ]
proof
let p be non zero Polynomial of R; :: thesis: ( deg p = 0 implies ex n being natural number st
( n = card () & n <= deg p ) )

assume A1: deg p = 0 ; :: thesis: ex n being natural number st
( n = card () & n <= deg p )

reconsider q = p as Element of the carrier of () by POLYNOM3:def 10;
consider a being Element of R such that
A2: q = a | R by ;
now :: thesis: ( Roots p <> {} implies for u being Element of Roots p holds contradiction )
assume A3: Roots p <> {} ; :: thesis: for u being Element of Roots p holds contradiction
let u be Element of Roots p; :: thesis: contradiction
u in Roots p by A3;
then reconsider u = u as Element of R ;
u is_a_root_of p by ;
then eval (p,u) = 0. R by POLYNOM5:def 7;
then a = 0. R by ;
hence contradiction by A2; :: thesis: verum
end;
hence ex n being natural number st
( n = card () & n <= deg p ) ; :: thesis: verum
end;
IS: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume IV: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for p being non zero Polynomial of R st deg p = k + 1 holds
ex n being natural number st
( n = card () & n <= deg p )
let p be non zero Polynomial of R; :: thesis: ( deg p = k + 1 implies ex n being natural number st
( b2 = card () & b2 <= deg n ) )

assume A1: deg p = k + 1 ; :: thesis: ex n being natural number st
( b2 = card () & b2 <= deg n )

per cases ( ex x being Element of R st x is_a_root_of p or for x being Element of R holds not x is_a_root_of p ) ;
suppose ex x being Element of R st x is_a_root_of p ; :: thesis: ex n being natural number st
( b2 = card () & b2 <= deg n )

then consider x being Element of R such that
A2: x is_a_root_of p ;
consider q being Polynomial of R such that
A3: p = (rpoly (1,x)) *' q by ;
A4: q <> 0_. R by A3;
reconsider q = q as non zero Polynomial of R by A3;
A7: deg p = (deg q) + (deg (rpoly (1,x))) by
.= (deg q) + 1 by HURWITZ:27 ;
then consider m being natural number such that
A5: ( m = card () & m <= deg q ) by A1, IV;
reconsider RQ = Roots q as finite Subset of R ;
now :: thesis: ( ( x in Roots q & ex n being natural number st
( n = card () & n <= deg p ) ) or ( not x in Roots q & ex n being natural number st
( n = card () & n <= deg p ) ) )
per cases ( x in Roots q or not x in Roots q ) ;
case x in Roots q ; :: thesis: ex n being natural number st
( n = card () & n <= deg p )

then for o being object st o in {x} holds
o in Roots q by TARSKI:def 1;
then A6: card (RQ \/ {x}) = m by ;
Roots (rpoly (1,x)) = {x} by ro4;
then A8: card () = m by ;
deg q <= (deg q) + 1 by NAT_1:11;
hence ex n being natural number st
( n = card () & n <= deg p ) by ; :: thesis: verum
end;
case not x in Roots q ; :: thesis: ex n being natural number st
( n = card () & n <= deg p )

then A6: card (RQ \/ {x}) = m + 1 by ;
Roots (rpoly (1,x)) = {x} by ro4;
then card () = m + 1 by ;
hence ex n being natural number st
( n = card () & n <= deg p ) by ; :: thesis: verum
end;
end;
end;
hence ex n being natural number st
( n = card () & n <= deg p ) ; :: thesis: verum
end;
suppose A2: for x being Element of R holds not x is_a_root_of p ; :: thesis: ex n being natural number st
( b2 = card () & b2 <= deg n )

now :: thesis: ( Roots p <> {} implies for x being Element of Roots p holds contradiction )
assume A3: Roots p <> {} ; :: thesis: for x being Element of Roots p holds contradiction
let x be Element of Roots p; :: thesis: contradiction
x in Roots p by A3;
then reconsider x = x as Element of R ;
x is_a_root_of p by ;
hence contradiction by A2; :: thesis: verum
end;
hence ex n being natural number st
( n = card () & n <= deg p ) ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
I: for k being Nat holds S1[k] from NAT_1:sch 2(IA, IS);
p <> 0_. R ;
then deg p is Element of NAT by T8;
hence ex n being natural number st
( n = card () & n <= deg p ) by I; :: thesis: verum