let F be ordered Field; :: thesis: for P being Ordering of F
for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
deg p is even
let P be Ordering of F; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
deg p is even
let f be FinSequence of the carrier of (Polynom-Ring F); :: thesis: for p being non zero Polynomial of F st p = Sum f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
deg p is even
let p be non zero Polynomial of F; :: thesis: ( p = Sum f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) implies deg p is even )
assume AS: ( p = Sum f & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) ) ; :: thesis: deg p is even
defpred S₁[ Nat] means for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f & len f = $1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
( deg p is even & LC p in P );
IA: S₁[1]

proof

now :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f & len f = 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
( deg p is even & LC p in P )

let f be FinSequence of the carrier of (Polynom-Ring F); :: thesis: for p being non zero Polynomial of F st p = Sum f & len f = 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
( deg p is even & LC p in P )
let p be non zero Polynomial of F; :: thesis: ( p = Sum f & len f = 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) implies ( deg p is even & LC p in P ) )
assume A0: ( p = Sum f & len f = 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) ) ; :: thesis: ( deg p is even & LC p in P )
then A1: f = <*(f . 1)*> by FINSEQ_1:40;
then dom f = {1} by FINSEQ_1:38, FINSEQ_1:2;
then reconsider e = 1 as Element of dom f by TARSKI:def 1;
A2: ( f . e in rng f & rng f c= the carrier of (Polynom-Ring F) ) by A1, FUNCT_1:3;
then reconsider q = f . e as Polynomial of F by POLYNOM3:def 10;
( deg q is even & LC q in P ) by A0;
hence ( deg p is even & LC p in P ) by A0, A1, A2, 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 non zero Polynomial of F st p = Sum f & len f = k + 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
( deg p is even & LC p in P )

let f be FinSequence of the carrier of (Polynom-Ring F); :: thesis: for p being non zero Polynomial of F st p = Sum f & len f = k + 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) holds
( deg b₃ is even & LC b₃ in P )
let p be non zero Polynomial of F; :: thesis: ( p = Sum f & len f = k + 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) implies ( deg b₂ is even & LC b₂ in P ) )
assume AS3: ( p = Sum f & len f = k + 1 & ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
( deg q is even & LC q in P ) ) ) ; :: thesis: ( deg b₂ is even & LC b₂ in P )
then f <> {} ;
then consider G being FinSequence, y being object such that
A1: f = G ^ <*y*> by FINSEQ_1:46;
rng G c= rng f by A1, FINSEQ_1:29;
then reconsider G = G as FinSequence of the carrier of (Polynom-Ring F) by XBOOLE_1:1, FINSEQ_1:def 4;
A5: rng f c= the carrier of (Polynom-Ring F) ;
A6: rng <*y*> c= rng f by A1, FINSEQ_1:30;
( rng <*y*> = {y} & y in {y} ) by FINSEQ_1:38, TARSKI:def 1;
then reconsider y = y as Element of the carrier of (Polynom-Ring F) by A5, A6;
A3: len f = (len G) + (len <*y*>) by A1, 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 AS3, AS1;
A4: Sum f = (Sum G) + (Sum <*y*>) by A1, RLVECT_1:41;
reconsider qG = Sum G, qy = y as Polynomial of F by POLYNOM3:def 10;
A7: ( deg qy is even & LC qy in P )

proof

dom <*y*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*y*> by FINSEQ_1:3;
then C: f . ((len G) + 1) = <*y*> . 1 by A1, FINSEQ_1:def 7
.= y ;
( 1 <= (len G) + 1 & dom f = Seg ((len G) + 1) ) by NAT_1:11, A3, FINSEQ_1:def 3;
then (len G) + 1 in dom f by FINSEQ_1:1;
hence ( deg qy is even & LC qy in P ) by C, AS3; :: thesis: verum

end;

per cases ( not qG is zero or qG is zero ) ;

suppose not qG is zero ; :: thesis: ( deg b₂ is even & LC b₂ in P )

then reconsider qG = qG as non zero Polynomial of F ;

C0: now :: thesis: for i being Element of dom G
for q being Polynomial of F st q = G . i holds
( deg q is even & LC q in P )

let i be Element of dom G; :: thesis: for q being Polynomial of F st q = G . i holds
( deg q is even & LC q in P )
let q be Polynomial of F; :: thesis: ( q = G . i implies ( deg q is even & LC q in P ) )
assume B1: q = G . i ; :: thesis: ( deg q is even & LC q in P )
( dom G c= dom f & i in dom G ) by A1, FINSEQ_1:26;
then ( f . i = G . i & i in dom f ) by A1, FINSEQ_1:def 7;
hence ( deg q is even & LC q in P ) by B1, AS3; :: thesis: verum

end;

then C1: ( deg qG is even & LC qG in P ) by A3, AS2, AS3;
not LC qG in {(0. F)} by TARSKI:def 1;
then C3: LC qG in P ^+ by C1, XBOOLE_0:def 5;
C9: ( (LC qG) + (LC qy) in (P ^+) + P & (P ^+) + P c= P ^+ ) by C3, A7, lemP;
not (LC qG) + (LC qy) in {(0. F)} by C9, XBOOLE_0:def 5;
then C2: (LC qG) + (LC qy) <> 0. F by TARSKI:def 1;
then C3: deg (qG + qy) = max ((deg qG),(deg qy)) by lem23a;
C4: p = (Sum G) + y by AS3, A4, RLVECT_1:44
.= qG + qy by POLYNOM3:def 10 ;
thus deg p is even :: thesis: LC p in P

proof

per cases ( deg (qG + qy) = deg qG or deg (qG + qy) = deg qy ) by C3, XXREAL_0:16;

suppose deg (qG + qy) = deg qG ; :: thesis: deg p is even

hence deg p is even by C4, C0, A3, AS2, AS3; :: thesis: verum

end;

suppose deg (qG + qy) = deg qy ; :: thesis: deg p is even

hence deg p is even by C4, A7; :: thesis: verum

end;

end;

end;

LC (qG + qy) in P

proof

per cases ( deg qG > deg qy or deg qG < deg qy or deg qG = deg qy ) by XXREAL_0:1;

suppose deg qG > deg qy ; :: thesis: LC (qG + qy) in P

hence LC (qG + qy) in P by C1, lem23d; :: thesis: verum

end;

suppose deg qG < deg qy ; :: thesis: LC (qG + qy) in P

hence LC (qG + qy) in P by A7, lem23d; :: thesis: verum

end;

suppose deg qG = deg qy ; :: thesis: LC (qG + qy) in P

then LC (qG + qy) = (LC qG) + (LC qy) by C2, lem23d;
hence LC (qG + qy) in P by C9, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence LC p in P by C4; :: thesis: verum

end;

suppose qG is zero ; :: thesis: ( deg b₂ is even & LC b₂ in P )

then qG = 0_. F by UPROOTS:def 5
.= 0. (Polynom-Ring F) by POLYNOM3:def 10 ;
hence ( deg p is even & LC p in P ) by A7, A4, AS3, RLVECT_1:44; :: thesis: verum

end;

end;

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);
p <> 0_. F ;
then p <> 0. (Polynom-Ring F) by POLYNOM3:def 10;
then f <> <*> the carrier of (Polynom-Ring F) by AS, RLVECT_1:43;
then len f >= 0 + 1 by INT_1:7;
hence deg p is even by AS, I; :: thesis: verum