set M = { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;
X:
FAdj (F,{a}) is Subring of E
by FIELD_5:12;
deg (MinPoly (a,F)) > 0
by RING_4:def 4;
then A:
a |^ 0 in { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) }
;
now for o being object st o in { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } holds
o in the carrier of (VecSp ((FAdj (F,{a})),F))let o be
object ;
( o in { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } implies o in the carrier of (VecSp ((FAdj (F,{a})),F)) )assume
o in { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) }
;
o in the carrier of (VecSp ((FAdj (F,{a})),F))then consider n being
Element of
NAT such that H:
(
o = a |^ n &
n < deg (MinPoly (a,F)) )
;
I:
the
carrier of
(VecSp ((FAdj (F,{a})),F)) = the
carrier of
(FAdj (F,{a}))
by FIELD_4:def 6;
reconsider U =
{a} as
Subset of
E ;
K:
{a} is
Subset of the
carrier of
(FAdj (F,{a}))
by FAt;
a in {a}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
(FAdj (F,{a})) by K;
a1 |^ n in the
carrier of
(FAdj (F,{a}))
;
hence
o in the
carrier of
(VecSp ((FAdj (F,{a})),F))
by I, H, X, pr5;
verum end;
hence
{ (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } is non empty Subset of (VecSp ((FAdj (F,{a})),F))
by A, TARSKI:def 3; verum