let F be Field; :: thesis:
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis:
let a be F -algebraic Element of E; :: thesis:
let p be Polynomial of F; :: thesis:
assume ASdeg: deg p < deg (MinPoly (a,F)) ; :: thesis:
H0: F is Subring of E by FIELD_4:def 1;
set V = VecSp ((FAdj (F,{a})),F);
set ma = MinPoly (a,F);
set K = FAdj (F,{a});
deg (MinPoly (a,F)) >= 0 + 1 by INT_1:7, RING_4:def 4;
then reconsider degma = (deg (MinPoly (a,F))) - 1 as Element of NAT by INT_1:3;
H0a: F is Subring of FAdj (F,{a}) by FIELD_4:def 1;

per cases ;

suppose p = 0_. F ; :: thesis:

then H: Ext_eval (p,a) = 0. E by ALGNUM_1:13
.= 0. (FAdj (F,{a})) by dFA
.= 0. (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 6
.= Sum (ZeroLC (VecSp ((FAdj (F,{a})),F))) by VECTSP_6:15 ;
ZeroLC (VecSp ((FAdj (F,{a})),F)) is Linear_Combination of Base a by VECTSP_6:5;
hence Ext_eval (p,a) in Lin (Base a) by H, VECTSP_7:7; :: thesis:

end;

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

defpred S₁[ Nat] means for p being Polynomial of F st deg p = $1 holds
Ext_eval (p,a) in Lin (Base a);
IA: S₁[ 0 ]

proof

now :: thesis:

let p be Polynomial of F; :: thesis:
assume AS1: deg p = 0 ; :: thesis:
then AS: p is constant by RATFUNC1:def 2;
defpred S₂[ object , object ] means ( ( $1 = a |^ 0 & $2 = p . 0 ) or ( $1 <> a |^ 0 & $2 = 0. F ) );
A: for x being object st x in the carrier of (VecSp ((FAdj (F,{a})),F)) holds
ex y being object st
( y in the carrier of F & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of (VecSp ((FAdj (F,{a})),F)) ; :: thesis:

per cases ;

suppose x = a |^ 0 ; :: thesis:

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis:

end;

suppose x <> a |^ 0 ; :: thesis:

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis:

end;

consider l being Function of the carrier of (VecSp ((FAdj (F,{a})),F)), the carrier of F such that
L: for x being object st x in the carrier of (VecSp ((FAdj (F,{a})),F)) holds
S₂[x,l . x] from FUNCT_2:sch 1(A);
reconsider l = l as Element of Funcs ( the carrier of (VecSp ((FAdj (F,{a})),F)), the carrier of F) by FUNCT_2:8;
A2: not deg (MinPoly (a,F)) <= 0 by RING_4:def 4;
for v being Element of (VecSp ((FAdj (F,{a})),F)) st not v in Base a holds
l . v = 0. F

proof

let v be Element of (VecSp ((FAdj (F,{a})),F)); :: thesis:
assume not v in Base a ; :: thesis:
then v <> a |^ 0 by A2;
hence l . v = 0. F by L; :: thesis:

end;

then reconsider l = l as Linear_Combination of VecSp ((FAdj (F,{a})),F) by VECTSP_6:def 1;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l ; :: thesis:
then consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
A1: ( o = v & l . v <> 0. F ) by VECTSP_6:1;
( v = a |^ 0 & l . v = p . 0 ) by L, A1;
hence o in Base a by A1, A2; :: thesis:

end;

then Carrier l c= Base a ;
then reconsider l = l as Linear_Combination of Base a by VECTSP_6:def 4;
A6: a |^ 0 = 1_ E by BINOM:8
.= 1. F by H0, C0SP1:def 3 ;
then A8: a |^ 0 = 1. (FAdj (F,{a})) by H0a, C0SP1:def 3;
then reconsider v = a |^ 0 as Element of (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 6;
the carrier of F c= the carrier of (FAdj (F,{a})) by H0a, C0SP1:def 3;
then reconsider p0 = p . 0 as Element of (FAdj (F,{a})) ;
reconsider a0 = a |^ 0 as Element of (FAdj (F,{a})) by A8;
A3: [(l . v),v] in [: the carrier of F, the carrier of (FAdj (F,{a})):] by A8, ZFMISC_1:def 2;
0 = (len p) - 1 by AS1, HURWITZ:def 2;
then A5: LC p = p . (1 -' 1) by RATFUNC1:def 6
.= p . (1 - 1) by XREAL_0:def 2 ;
A7: [(p . 0),(1. F)] in [: the carrier of F, the carrier of F:] by ZFMISC_1:def 2;
A9: Carrier l = {v}

proof

Y: now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l ; :: thesis:
then consider w being Element of (VecSp ((FAdj (F,{a})),F)) such that
A9b: ( o = w & l . w <> 0. F ) by VECTSP_6:1;
o = v by A9b, L;
hence o in {v} by TARSKI:def 1; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume o in {v} ; :: thesis:
then A9c: o = v by TARSKI:def 1;
p <> 0_. F by AS1, HURWITZ:20;
then not p is zero by UPROOTS:def 5;
then l . v <> 0. F by L, A5;
hence o in Carrier l by A9c, VECTSP_6:1; :: thesis:

end;

hence Carrier l = {v} by TARSKI:2, Y; :: thesis:

end;

Sum l = (l . v) * v by A9, VECTSP_6:20
.= ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . ((l . v),v) by FIELD_4:def 6
.= the multF of (FAdj (F,{a})) . ((l . v),v) by A3, FUNCT_1:49
.= the multF of (FAdj (F,{a})) . ((p . 0),(1. F)) by L, A6
.= ( the multF of (FAdj (F,{a})) || the carrier of F) . ((p . 0),(1. F)) by A7, FUNCT_1:49
.= (p . 0) * (1. F) by H0a, C0SP1:def 3
.= Ext_eval (p,a) by A5, AS, exevalconst ;
hence Ext_eval (p,a) in Lin (Base a) by VECTSP_7:7; :: thesis:

end;

hence S₁[ 0 ] ; :: thesis:

end;

IS: for k being Element of NAT st 0 <= k & k < degma & ( for j being Element of NAT st 0 <= j & j <= k holds
S₁[j] ) holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume IV0: ( 0 <= k & k < degma ) ; :: thesis:
assume IV1: for j being Element of NAT st 0 <= j & j <= k holds
S₁[j] ; :: thesis:

now :: thesis:

let p be Polynomial of F; :: thesis:
assume IS0: deg p = k + 1 ; :: thesis:
IS: deg p = (len p) - 1 by HURWITZ:def 2;
then len p <> 0 by IS0;
then consider r being Polynomial of F such that
IS1: ( len r < len p & p = r + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
r . n = p . n ) ) by POLYNOM4:16;
(len r) - 1 < (len p) - 1 by IS1, XREAL_1:9;
then IS3: deg r < deg p by IS, HURWITZ:def 2;
IS4: k + 1 < degma + 1 by IV0, XREAL_1:8;

per cases ;

suppose r = 0_. F ; :: thesis:

hence Ext_eval (p,a) in Lin (Base a) by IS1, IS4, IS0, lembas1b; :: thesis:

end;

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

then reconsider degr = deg r as Element of NAT by FIELD_1:1;
degr <= k by IS3, IS0, NAT_1:13;
then consider lr being Linear_Combination of Base a such that
IS5: Ext_eval (r,a) = Sum lr by IV1, VECTSP_7:7;
set LMp = Leading-Monomial p;
Ext_eval ((Leading-Monomial p),a) in Lin (Base a) by IS4, IS0, lembas1b;
then consider l being Linear_Combination of Base a such that
IS6: Ext_eval ((Leading-Monomial p),a) = Sum l by VECTSP_7:7;
reconsider ls = l + lr as Linear_Combination of Base a by VECTSP_6:24;
Ext_eval ((Leading-Monomial p),a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
then Ext_eval ((Leading-Monomial p),a) in RAdj (F,{a}) by lemphi5;
then IS8: Ext_eval ((Leading-Monomial p),a) in FAdj (F,{a}) by ch1;
Ext_eval (r,a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
then Ext_eval (r,a) in RAdj (F,{a}) by lemphi5;
then Ext_eval (r,a) in FAdj (F,{a}) by ch1;
then IS7: [(Sum l),(Sum lr)] in [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{a})):] by IS5, IS6, IS8, ZFMISC_1:def 2;
Sum ls = (Sum l) + (Sum lr) by VECTSP_6:44
.= the addF of (FAdj (F,{a})) . ((Sum l),(Sum lr)) by FIELD_4:def 6
.= ( the addF of E || the carrier of (FAdj (F,{a}))) . ((Sum l),(Sum lr)) by EC_PF_1:def 1
.= (Ext_eval ((Leading-Monomial p),a)) + (Ext_eval (r,a)) by IS5, IS6, IS7, FUNCT_1:49
.= Ext_eval (p,a) by IS1, H0, ALGNUM_1:15 ;
hence Ext_eval (p,a) in Lin (Base a) by VECTSP_7:7; :: thesis:

end;

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

end;

I: for j being Element of NAT st 0 <= j & j <= degma holds
S₁[j] from INT_1:sch 8(IA, IS);
reconsider degp = deg p as Element of NAT by FIELD_1:1, X;
degp + 1 <= deg (MinPoly (a,F)) by ASdeg, INT_1:7;
then (degp + 1) - 1 <= (deg (MinPoly (a,F))) - 1 by XREAL_1:9;
hence Ext_eval (p,a) in Lin (Base a) by I; :: thesis:

end;