suppose p <> 0_. F ; :: thesis:

b in Support (Poly (m,p)) by AS, TARSKI:def 1;
then H3: p . (b . m) <> 0. F by POLYNOM1:def 3, AS1;
reconsider i = b . m as Element of NAT ;

let o be object ; :: thesis:
assume H0: o in Support p ; :: thesis:
then reconsider u = o as Element of NAT ;
H4: p . u <> 0. F by H0, POLYNOM1:def 3;

H5: now :: thesis:

assume H6: u <> i ; :: thesis:
for o being object st o in {m} holds
o in card (nonConstantPolys F) by AS0, TARSKI:def 1;
then reconsider S = {m} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
set b1 = (S,u) -bag ;
set b2 = (S,i) -bag ;
J: m in S by TARSKI:def 1;

per cases ;

suppose H7: u = 0 ; :: thesis:

then H12: (S,u) -bag = EmptyBag (card (nonConstantPolys F)) by UPROOTS:9;
then H8: (Poly (m,p)) . ((S,u) -bag) = p . u by H7, defPg;
support ((S,i) -bag) = S by H7, H6, UPROOTS:8;
then H9: (Poly (m,p)) . ((S,i) -bag) = p . (((S,i) -bag) . m) by defPg
.= p . i by J, UPROOTS:7 ;
((S,i) -bag) . m = i by J, UPROOTS:7;
then (S,i) -bag <> EmptyBag (card (nonConstantPolys F)) by H7, H6, PBOOLE:5;
then H10: card {((S,u) -bag),((S,i) -bag)} = 2 by H12, CARD_2:57;
{((S,u) -bag),((S,i) -bag)} c= Support (Poly (m,p))

proof

now :: thesis:

let o be object ; :: thesis:
assume o in {((S,u) -bag),((S,i) -bag)} ; :: thesis:

per cases by TARSKI:def 2;

suppose o = (S,u) -bag ; :: thesis:

hence o in Support (Poly (m,p)) by H8, H4, POLYNOM1:def 4; :: thesis:

end;

suppose o = (S,i) -bag ; :: thesis:

hence o in Support (Poly (m,p)) by H9, H3, POLYNOM1:def 4; :: thesis:

end;

hence {((S,u) -bag),((S,i) -bag)} c= Support (Poly (m,p)) ; :: thesis:

end;

hence card (Support (Poly (m,p))) >= 2 by H10, NAT_1:43; :: thesis:

end;

suppose H7a: u <> 0 ; :: thesis:

then support ((S,u) -bag) = S by UPROOTS:8;
then H9: (Poly (m,p)) . ((S,u) -bag) = p . (((S,u) -bag) . m) by defPg
.= p . u by J, UPROOTS:7 ;

per cases ;

suppose H11: i = 0 ; :: thesis:

then H12: (S,i) -bag = EmptyBag (card (nonConstantPolys F)) by UPROOTS:9;
then H8: (Poly (m,p)) . ((S,i) -bag) = p . i by H11, defPg;
((S,u) -bag) . m = u by J, UPROOTS:7;
then (S,u) -bag <> EmptyBag (card (nonConstantPolys F)) by H7a, PBOOLE:5;
then H10: card {((S,u) -bag),((S,i) -bag)} = 2 by H12, CARD_2:57;
{((S,u) -bag),((S,i) -bag)} c= Support (Poly (m,p))

proof

now :: thesis:

let o be object ; :: thesis:
assume o in {((S,u) -bag),((S,i) -bag)} ; :: thesis:

per cases by TARSKI:def 2;

suppose o = (S,u) -bag ; :: thesis:

hence o in Support (Poly (m,p)) by H9, H4, POLYNOM1:def 4; :: thesis:

end;

suppose o = (S,i) -bag ; :: thesis:

hence o in Support (Poly (m,p)) by H8, H3, POLYNOM1:def 4; :: thesis:

end;

hence {((S,u) -bag),((S,i) -bag)} c= Support (Poly (m,p)) ; :: thesis:

end;

hence card (Support (Poly (m,p))) >= 2 by H10, NAT_1:43; :: thesis:

end;

suppose i <> 0 ; :: thesis:

then support ((S,i) -bag) = S by UPROOTS:8;
then H9a: (Poly (m,p)) . ((S,i) -bag) = p . (((S,i) -bag) . m) by defPg
.= p . i by J, UPROOTS:7 ;
( ((S,u) -bag) . m = u & ((S,i) -bag) . m = i ) by J, UPROOTS:7;
then H10: card {((S,u) -bag),((S,i) -bag)} = 2 by H6, CARD_2:57;
{((S,u) -bag),((S,i) -bag)} c= Support (Poly (m,p))

proof

now :: thesis:

let o be object ; :: thesis:
assume o in {((S,u) -bag),((S,i) -bag)} ; :: thesis:

per cases by TARSKI:def 2;

suppose o = (S,u) -bag ; :: thesis:

hence o in Support (Poly (m,p)) by H9, H4, POLYNOM1:def 4; :: thesis:

end;

suppose o = (S,i) -bag ; :: thesis:

hence o in Support (Poly (m,p)) by H9a, H3, POLYNOM1:def 4; :: thesis:

end;

hence {((S,u) -bag),((S,i) -bag)} c= Support (Poly (m,p)) ; :: thesis:

end;

hence card (Support (Poly (m,p))) >= 2 by H10, NAT_1:43; :: thesis:

end;

card (Support (Poly (m,p))) = 1 by AS, CARD_1:30;
hence o = b . m by H5; :: thesis:

end;

consider G being FinSequence of E such that
A1: ( Ext_eval (p,a) = Sum G & len G = len p & ( for n being Element of NAT st n in dom G holds
G . n = (In ((p . (n -' 1)),E)) * ((power E) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;

A2: now :: thesis:

let j be Element of NAT ; :: thesis:
assume A3: ( j in dom G & j <> i + 1 ) ; :: thesis:
H: F is Subring of E by FIELD_4:def 1;

now :: thesis:

assume A4: j -' 1 = i ; :: thesis:
j in Seg (len G) by A3, FINSEQ_1:def 3;
then ( 1 <= j & j <= len G ) by FINSEQ_1:1;
then j -' 1 = j - 1 by XREAL_0:def 2;
hence contradiction by A3, A4; :: thesis:

end;

then not j -' 1 in Support p by AA;
then p . (j -' 1) = 0. F by POLYNOM1:def 4
.= 0. E by H, C0SP1:def 3 ;
then (In ((p . (j -' 1)),E)) * ((power E) . (a,(j -' 1))) = 0. E ;
hence 0. E = G . j by A1, A3
.= G /. j by A3, PARTFUN1:def 6 ;
:: thesis:

end;

( 1 <= i + 1 & i + 1 <= len p ) by H3, NAT_1:11, NAT_1:13, ALGSEQ_1:8;
then i + 1 in Seg (len G) by A1;
then A3: i + 1 in dom G by FINSEQ_1:def 3;
A5: (i + 1) -' 1 = (i + 1) - 1 by NAT_1:11, XREAL_1:233;
A4: Ext_eval (p,a) = G /. (i + 1) by A3, A2, A1, POLYNOM2:3
.= G . (i + 1) by A3, PARTFUN1:def 6
.= (In ((p . i),E)) * ((power E) . (a,i)) by A5, A3, A1 ;

per cases ;

suppose support b = {} ; :: thesis:

then A6: b = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
then A5: ( b . m = 0 & eval (b,x) = 1. E ) by PBOOLE:5, POLYNOM2:14;
thus Ext_eval ((Poly (m,p)),x) = (In ((p . i),E)) * (1_ E) by Z, A6, POLYNOM2:14
.= (In ((p . i),E)) * ((power E) . (a,i)) by A5, GROUP_1:def 7
.= Ext_eval (p,(x /. m)) by A4, Y, PARTFUN1:def 6 ; :: thesis:

end;

suppose support b <> {} ; :: thesis:

then b <> EmptyBag (card (nonConstantPolys F)) ;
then A6: ( not b in {(EmptyBag (card (nonConstantPolys F)))} & b in Support (Poly (m,p)) ) by AS, TARSKI:def 1;
Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } by Th14c;
then b in { b where b is bag of card (nonConstantPolys F) : support b = {m} } by A6, XBOOLE_0:def 3;
then consider b1 being bag of card (nonConstantPolys F) such that
A5: ( b1 = b & support b1 = {m} ) ;
thus Ext_eval ((Poly (m,p)),x) = (In ((p . i),E)) * ((power E) . (a,i)) by A5, Z, POLYNOM2:15
.= Ext_eval (p,(x /. m)) by A4, Y, PARTFUN1:def 6 ; :: thesis:

end;