let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being F -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))
let a be F -algebraic Element of E; :: thesis: Base a is Basis of (VecSp ((FAdj (F,{a})),F))
set V = VecSp ((FAdj (F,{a})),F);
set ma = MinPoly (a,F);
H0: F is Subring of E by FIELD_4:def 1;

A: now :: thesis: for l being Linear_Combination of Base a st Sum l = 0. (VecSp ((FAdj (F,{a})),F)) holds
Carrier l = {}

let l be Linear_Combination of Base a; :: thesis: ( Sum l = 0. (VecSp ((FAdj (F,{a})),F)) implies Carrier l = {} )
assume A1: Sum l = 0. (VecSp ((FAdj (F,{a})),F)) ; :: thesis: Carrier l = {}
0. (VecSp ((FAdj (F,{a})),F)) = 0. (FAdj (F,{a})) by FIELD_4:def 6
.= 0. E by dFA
.= 0. F by H0, C0SP1:def 3 ;
then l = ZeroLC (VecSp ((FAdj (F,{a})),F)) by A1, lembas2;
hence Carrier l = {} by VECTSP_6:def 3; :: thesis: verum

end;

E: now :: thesis: for o being object st o in the carrier of ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) holds
o in the carrier of (Lin (Base a))

let o be object ; :: thesis: ( o in the carrier of ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) implies o in the carrier of (Lin (Base a)) )
assume o in the carrier of ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) ; :: thesis: o in the carrier of (Lin (Base a))
then o in the carrier of (FAdj (F,{a})) by FIELD_4:def 6;
then o in the carrier of (RAdj (F,{a})) by ch1;
then o in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by lemphi5;
then consider p being Polynomial of F such that
A1: o = Ext_eval (p,a) ;
o in Lin (Base a) by A1, lembas1;
hence o in the carrier of (Lin (Base a)) ; :: thesis: verum

end;

now :: thesis: for o being object st o in the carrier of (Lin (Base a)) holds
o in the carrier of (VecSp ((FAdj (F,{a})),F))

let o be object ; :: thesis: ( o in the carrier of (Lin (Base a)) implies o in the carrier of (VecSp ((FAdj (F,{a})),F)) )
assume G: o in the carrier of (Lin (Base a)) ; :: thesis: o in the carrier of (VecSp ((FAdj (F,{a})),F))
the carrier of (Lin (Base a)) c= the carrier of (VecSp ((FAdj (F,{a})),F)) by VECTSP_4:def 2;
hence o in the carrier of (VecSp ((FAdj (F,{a})),F)) by G; :: thesis: verum

end;

then Lin (Base a) = ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) by VECTSP_4:31, E, TARSKI:2;
hence Base a is Basis of (VecSp ((FAdj (F,{a})),F)) by A, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum