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

proof

let p be non zero Polynomial of R; :: thesis:
assume A1: deg p = 0 ; :: thesis:
reconsider q = p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
consider a being Element of R such that
A2: q = a | R by A1, RING_4:def 4, RING_4:20;

now :: thesis:

assume A3: Roots p <> {} ; :: thesis:
let u be Element of Roots p; :: thesis:
u in Roots p by A3;
then reconsider u = u as Element of R ;
u is_a_root_of p by A3, POLYNOM5:def 10;
then eval (p,u) = 0. R by POLYNOM5:def 7;
then a = 0. R by A2, evconst;
hence contradiction by A2; :: thesis:

end;

hence ex n being natural number st
( n = card (Roots p) & n <= deg p ) ; :: thesis:

end;

IS: now :: thesis:

let k be Nat; :: thesis:
assume IV: S₁[k] ; :: thesis:

now :: thesis:

let p be non zero Polynomial of R; :: thesis:
assume A1: deg p = k + 1 ; :: thesis:

per cases ;

suppose ex x being Element of R st x is_a_root_of p ; :: thesis:

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 A2, HURWITZ:33;
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 HURWITZ:23, A3, A4
.= (deg q) + 1 by HURWITZ:27 ;
then consider m being natural number such that
A5: ( m = card (Roots q) & m <= deg q ) by A1, IV;
reconsider RQ = Roots q as finite Subset of R ;

now :: thesis:

per cases ;

case x in Roots q ; :: thesis:

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 A5, XBOOLE_1:12, TARSKI:def 3;
Roots (rpoly (1,x)) = {x} by ro4;
then A8: card (Roots p) = m by A3, A6, UPROOTS:23;
deg q <= (deg q) + 1 by NAT_1:11;
hence ex n being natural number st
( n = card (Roots p) & n <= deg p ) by A7, A8, A5, XXREAL_0:2; :: thesis:

end;

case not x in Roots q ; :: thesis:

then A6: card (RQ \/ {x}) = m + 1 by A5, CARD_2:41;
Roots (rpoly (1,x)) = {x} by ro4;
then card (Roots p) = m + 1 by A3, A6, UPROOTS:23;
hence ex n being natural number st
( n = card (Roots p) & n <= deg p ) by A7, A5, XREAL_1:6; :: thesis:

end;

end;

end;

hence ex n being natural number st
( n = card (Roots p) & n <= deg p ) ; :: thesis:

end;

suppose A2: for x being Element of R holds not x is_a_root_of p ; :: thesis:

now :: thesis:

assume A3: Roots p <> {} ; :: thesis:
let x be Element of Roots p; :: thesis:
x in Roots p by A3;
then reconsider x = x as Element of R ;
x is_a_root_of p by A3, POLYNOM5:def 10;
hence contradiction by A2; :: thesis:

end;

hence ex n being natural number st
( n = card (Roots p) & n <= deg p ) ; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

I: for k being Nat holds S₁[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 (Roots p) & n <= deg p ) by I; :: thesis: