let F be Field; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let f be FinSequence of the carrier of (Polynom-Ring F); :: thesis: for p being non zero Polynomial of F st p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let p be non zero Polynomial of F; :: thesis: ( p = Sum f implies for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n )
assume AS1: p = Sum f ; :: thesis: for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let g be FinSequence of F; :: thesis: for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let n be Nat; :: thesis: ( ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) implies deg p <= n )
assume AS2: for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ; :: thesis: deg p <= n
defpred S₁[ Nat] means for f being FinSequence of the carrier of (Polynom-Ring F)
for p being Polynomial of F st len f = $1 & p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n;
IA: S₁[1]

proof

now :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F)
for p being Polynomial of F st len f = 1 & p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n

let f be FinSequence of the carrier of (Polynom-Ring F); :: thesis: for p being Polynomial of F st len f = 1 & p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let p be Polynomial of F; :: thesis: ( len f = 1 & p = Sum f implies for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n )
assume A1: ( len f = 1 & p = Sum f ) ; :: thesis: for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let g be FinSequence of F; :: thesis: for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let n be Nat; :: thesis: ( ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) implies deg p <= n )
assume A2: for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ; :: thesis: deg p <= n
A3: f = <*(f . 1)*> by A1, FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:38;
then A4: 1 in dom f by FINSEQ_1:2, TARSKI:def 1;
then A5: f . 1 in rng f by FUNCT_1:3;
then reconsider q = f . 1 as Polynomial of F by A1, A3, RLVECT_1:44;
thus deg p <= n by A5, A4, A2, A1, A3, RLVECT_1:44; :: thesis: verum

end;

hence S₁[1] ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st k >= 1 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume AS1: k >= 1 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume AS2: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F)
for p being Polynomial of F st len f = k + 1 & p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n

let f be FinSequence of the carrier of (Polynom-Ring F); :: thesis: for p being Polynomial of F st len f = k + 1 & p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let p be Polynomial of F; :: thesis: ( len f = k + 1 & p = Sum f implies for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n )
assume A1: ( len f = k + 1 & p = Sum f ) ; :: thesis: for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let g be FinSequence of F; :: thesis: for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n
let n be Nat; :: thesis: ( ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) implies deg p <= n )
assume A2: for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ; :: thesis: deg p <= n
f <> {} by A1;
then consider G being FinSequence, y being object such that
A3: f = G ^ <*y*> by FINSEQ_1:46;
rng G c= rng f by A3, FINSEQ_1:29;
then reconsider G = G as FinSequence of the carrier of (Polynom-Ring F) by XBOOLE_1:1, FINSEQ_1:def 4;
A4: len f = (len G) + (len <*y*>) by A3, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
then reconsider G = G as non empty FinSequence of the carrier of (Polynom-Ring F) by AS1, A1;
reconsider r = Sum G as Polynomial of F by POLYNOM3:def 10;

now :: thesis: for i being Element of dom G
for q being Polynomial of F st q = G . i holds
deg q <= n

let i be Element of dom G; :: thesis: for q being Polynomial of F st q = G . i holds
deg q <= n
let q be Polynomial of F; :: thesis: ( q = G . i implies deg q <= n )
assume B1: q = G . i ; :: thesis: deg q <= n
B2: ( i in dom G & dom G c= dom f ) by A3, FINSEQ_1:26;
G . i = f . i by A3, FINSEQ_1:def 7;
hence deg q <= n by B1, B2, A2; :: thesis: verum

end;

then A5: deg r <= n by A1, A4, AS2;
rng <*y*> = {y} by FINSEQ_1:39;
then A6: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng f by A3, FINSEQ_1:30;
then consider u being object such that
A7: ( u in dom f & f . u = y ) by A6, FUNCT_1:def 3;
reconsider u = u as Element of NAT by A7;
( f . u in rng f & rng f c= the carrier of (Polynom-Ring F) ) by A7, FUNCT_1:3;
then reconsider y = y as Element of the carrier of (Polynom-Ring F) by A7;
reconsider s = y as Polynomial of F ;
A8: Sum <*y*> = s by RLVECT_1:44;
( dom f = Seg ((len G) + 1) & 1 <= (len G) + 1 ) by A4, FINSEQ_1:def 3, NAT_1:11;
then A9: (len G) + 1 in dom f by FINSEQ_1:1;
f . ((len G) + 1) = y by A3, FINSEQ_1:42;
then A10: deg s <= n by A2, A9;
p = (Sum G) + (Sum <*y*>) by A1, A3, RLVECT_1:41
.= r + s by A8, POLYNOM3:def 10 ;
then A11: deg p <= max ((deg r),(deg s)) by HURWITZ:22;
max ((deg r),(deg s)) <= n by A5, A10, XXREAL_0:28;
hence deg p <= n by A11, XXREAL_0:2; :: thesis: verum

end;

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

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);

now :: thesis: not f = {}

assume f = {} ; :: thesis: contradiction
then f = <*> the carrier of (Polynom-Ring F) ;
then ( Sum f = 0. (Polynom-Ring F) & p <> 0_. F ) by RLVECT_1:43;
hence contradiction by AS1, POLYNOM3:def 10; :: thesis: verum

end;

then len f >= 0 + 1 by INT_1:7;
hence deg p <= n by I, AS1, AS2; :: thesis: verum