begin
scheme
IndFinSeq0{
F1()
-> Nat,
P1[
set ] } :
provided
A1:
P1[1]
and A2:
for
i being
Element of
NAT st 1
<= i &
i < F1() &
P1[
i] holds
P1[
i + 1]
begin
begin
begin
begin
Lm1:
now for L being domRing
for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
let L be
domRing;
for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )let p be
non-zero Polynomial of
L;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )defpred S1[
Nat]
means for
p being
Polynomial of
L st
len p = $1 holds
(
Roots p is
finite & ex
n being
Element of
NAT st
(
n = card (Roots p) &
n < len p ) );
p <> 0_. L
by Def5;
then
len p <> 0
by POLYNOM4:5;
then A1:
len p >= 0 + 1
by NAT_1:13;
A2:
for
n being
Nat st
n >= 1 &
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A3:
S1[
n]
;
S1[n + 1]
let p be
Polynomial of
L;
( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) ) )
assume A4:
len p = n + 1
;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
per cases
( p is with_roots or not p is with_roots )
;
suppose
p is
with_roots
;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
then consider x being
Element of
L such that A5:
x is_a_root_of p
by POLYNOM5:def 7;
set r =
<%(- x),(1. L)%>;
set pq =
poly_quotient (
p,
x);
A6:
p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
by A5, Th50;
then A7:
Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x)))
by Th23;
A8:
Roots <%(- x),(1. L)%> = {x}
by Th48;
then reconsider Rr =
Roots <%(- x),(1. L)%> as
finite set ;
A9:
(len (poly_quotient (p,x))) + 1
= len p
by A4, A5, Def7;
then consider k being
Element of
NAT such that A10:
k = card (Roots (poly_quotient (p,x)))
and A11:
k < len (poly_quotient (p,x))
by A3, A4;
reconsider Rpq =
Roots (poly_quotient (p,x)) as
finite set by A3, A4, A9;
reconsider Rp =
Rpq \/ Rr as
finite set ;
card Rr = 1
by A8, CARD_1:30;
then A12:
card Rp <= k + 1
by A10, CARD_2:43;
Roots (poly_quotient (p,x)) is
finite
by A3, A4, A9;
hence
Roots p is
finite
by A8, A7;
ex n being Element of NAT st
( n = card (Roots p) & n < len p )take m =
card Rp;
( m = card (Roots p) & m < len p )thus
m = card (Roots p)
by A6, Th23;
m < len p
k + 1
< n + 1
by A4, A9, A11, XREAL_1:8;
hence
m < len p
by A4, A12, XXREAL_0:2;
verum
end;
end;
end;
A16:
S1[1]
for
n being
Nat st
n >= 1 holds
S1[
n]
from NAT_1:sch 8(A16, A2);
hence
(
Roots p is
finite & ex
n being
Element of
NAT st
(
n = card (Roots p) &
n < len p ) )
by A1;
verum
end;
begin