let F be Field; :: thesis: for E being FieldExtension of F
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
let E be FieldExtension of F; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m)) )
assume AS: m in card (nonConstantPolys F) ; :: thesis: for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
let p be Polynomial of F; :: thesis: for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
let x be Function of (card (nonConstantPolys F)),E; :: thesis: Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
set q = Poly (m,p);
set n = card (nonConstantPolys F);
defpred S₁[ Nat] means for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E st card (Support (Poly (m,p))) = $1 holds
Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m));

IS: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[b₁] )
assume IV: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[b₁]

per cases ( k = 0 or k <> 0 ) ;

suppose A: k = 0 ; :: thesis: S₁[b₁]

now :: thesis: for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E st card (Support (Poly (m,p))) = k holds
Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))

let p be Polynomial of F; :: thesis: for x being Function of (card (nonConstantPolys F)),E st card (Support (Poly (m,p))) = k holds
Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
let x be Function of (card (nonConstantPolys F)),E; :: thesis: ( card (Support (Poly (m,p))) = k implies Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m)) )
assume card (Support (Poly (m,p))) = k ; :: thesis: Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
then Support (Poly (m,p)) = {} by A;
then B: Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) by YY;
then C: p = 0_. F by AS, pZero;
thus Ext_eval ((Poly (m,p)),x) = 0. E by B, ev0
.= Ext_eval (p,(x /. m)) by C, ALGNUM_1:13 ; :: thesis: verum

end;

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

end;

suppose A: k <> 0 ; :: thesis: S₁[b₁]

then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
H: F is Subring of E by FIELD_4:def 1;

now :: thesis: for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E st card (Support (Poly (m,p))) = k holds
Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))

let p be Polynomial of F; :: thesis: for x being Function of (card (nonConstantPolys F)),E st card (Support (Poly (m,p))) = k holds
Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
let x be Function of (card (nonConstantPolys F)),E; :: thesis: ( card (Support (Poly (m,p))) = k implies Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m)) )
assume Z: card (Support (Poly (m,p))) = k ; :: thesis: Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))
set q = p - (LM p);
B: (LM p) + (p - (LM p)) = ((LM p) + (- (LM p))) + p by POLYNOM3:26
.= ((LM p) - (LM p)) + p
.= (0_. F) + p by POLYNOM3:29 ;
C: (LM (Poly (m,p))) + (Poly (m,(p - (LM p)))) = (LM (Poly (m,p))) + ((Poly (m,p)) + (Poly (m,(- (LM p))))) by Th14
.= (LM (Poly (m,p))) + ((Poly (m,p)) + (- (Poly (m,(LM p))))) by Th14xy
.= (LM (Poly (m,p))) + ((Poly (m,p)) + (- (LM (Poly (m,p))))) by AS, Th14y
.= ((LM (Poly (m,p))) + (- (LM (Poly (m,p))))) + (Poly (m,p)) by POLYNOM1:21
.= ((LM (Poly (m,p))) - (LM (Poly (m,p)))) + (Poly (m,p)) by POLYNOM1:def 7
.= (0_ ((card (nonConstantPolys F)),F)) + (Poly (m,p)) by POLYNOM1:24
.= Poly (m,p) by POLYNOM1:23 ;
Support (Poly (m,(p - (LM p)))) c< Support (Poly (m,p))

proof

Support (Poly (m,p)) <> {} by A, Z;
then LM (Poly (m,p)) <> 0_ ((card (nonConstantPolys F)),F) by YY, Z2a;
then C5: Support (LM (Poly (m,p))) = {(Lt (Poly (m,p)))} by YY, Z2;
then C8: Lt (Poly (m,p)) in Support (LM (Poly (m,p))) by TARSKI:def 1;
Support (LM (Poly (m,p))) c= Support (Poly (m,p)) by YZ;
then C4: Lt (Poly (m,p)) in Support (Poly (m,p)) by C8;
set b = Lt (Poly (m,p));
C7: (Poly (m,(p - (LM p)))) . (Lt (Poly (m,p))) = ((Poly (m,p)) + (Poly (m,(- (LM p))))) . (Lt (Poly (m,p))) by Th14
.= ((Poly (m,p)) . (Lt (Poly (m,p)))) + ((Poly (m,(- (LM p)))) . (Lt (Poly (m,p)))) by POLYNOM1:15
.= ((Poly (m,p)) . (Lt (Poly (m,p)))) + ((- (Poly (m,(LM p)))) . (Lt (Poly (m,p)))) by Th14xy
.= ((Poly (m,p)) . (Lt (Poly (m,p)))) + (- ((Poly (m,(LM p))) . (Lt (Poly (m,p))))) by POLYNOM1:17
.= (LC (Poly (m,p))) + (- ((LM (Poly (m,p))) . (Lt (Poly (m,p))))) by AS, Th14y
.= (LC (Poly (m,p))) + (- (LC (Poly (m,p)))) by lemY
.= 0. F by RLVECT_1:5 ;
then C6: not Lt (Poly (m,p)) in Support (Poly (m,(p - (LM p)))) by POLYNOM1:def 4;

now :: thesis: for o being object st o in Support (Poly (m,(p - (LM p)))) holds
o in Support (Poly (m,p))

let o be object ; :: thesis: ( o in Support (Poly (m,(p - (LM p)))) implies o in Support (Poly (m,p)) )
assume C0: o in Support (Poly (m,(p - (LM p)))) ; :: thesis: o in Support (Poly (m,p))
then reconsider b = o as bag of card (nonConstantPolys F) ;
C3: b is Element of Bags (card (nonConstantPolys F)) by PRE_POLY:def 12;
C1: (Poly (m,(p - (LM p)))) . b <> 0. F by C0, POLYNOM1:def 4;
then not b in Support (LM (Poly (m,p))) by C7, C5, TARSKI:def 1;
then not b in Support (Poly (m,(LM p))) by AS, Th14y;
then C2: (Poly (m,(LM p))) . b = 0. F by C3, POLYNOM1:def 4;
(Poly (m,(p - (LM p)))) . b = ((Poly (m,p)) + (Poly (m,(- (LM p))))) . b by Th14
.= ((Poly (m,p)) . b) + ((Poly (m,(- (LM p)))) . b) by POLYNOM1:15
.= ((Poly (m,p)) . b) + ((- (Poly (m,(LM p)))) . b) by Th14xy
.= ((Poly (m,p)) . b) + (- ((Poly (m,(LM p))) . b)) by POLYNOM1:17
.= (Poly (m,p)) . b by C2 ;
hence o in Support (Poly (m,p)) by C1, C3, POLYNOM1:def 4; :: thesis: verum

end;

then Support (Poly (m,(p - (LM p)))) c= Support (Poly (m,p)) ;
hence Support (Poly (m,(p - (LM p)))) c< Support (Poly (m,p)) by C6, C4, XBOOLE_0:def 8; :: thesis: verum

end;

then D: card (Support (Poly (m,(p - (LM p))))) < k by Z, CARD_2:48;
Support (Poly (m,p)) <> {} by A, Z;
then LM (Poly (m,p)) <> 0_ ((card (nonConstantPolys F)),F) by YY, Z2a;
then Support (LM (Poly (m,p))) <> {} by YY;
then Support (Poly (m,(LM p))) <> {} by AS, Th14y;
then ex b being bag of card (nonConstantPolys F) st Support (Poly (m,(LM p))) = {b} by POLYNOM7:6;
then E: card (Support (Poly (m,(LM p)))) = 1 by CARD_2:42;
thus Ext_eval ((Poly (m,p)),x) = (Ext_eval ((LM (Poly (m,p))),x)) + (Ext_eval ((Poly (m,(p - (LM p)))),x)) by H, C, evalpl
.= (Ext_eval ((LM (Poly (m,p))),x)) + (Ext_eval ((p - (LM p)),(x /. m))) by D, IV
.= (Ext_eval ((Poly (m,(LM p))),x)) + (Ext_eval ((p - (LM p)),(x /. m))) by AS, Th14y
.= (Ext_eval ((LM p),(x /. m))) + (Ext_eval ((p - (LM p)),(x /. m))) by AS, E, eval0LM
.= Ext_eval (p,(x /. m)) by B, H, ALGNUM_1:15 ; :: thesis: verum

end;

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

end;

end;

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(IS);
consider n being Nat such that
H: card (Support (Poly (m,p))) = n ;
thus Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m)) by I, H; :: thesis: verum