let E be F -finite FieldExtension of F; :: thesis: E is F -simple
set G = MultGroup E;
consider g being Element of (MultGroup E) such that
A: for b being Element of (MultGroup E) ex n being Nat st b = g |^ n by GR_CY_1:18;
B: the carrier of E = the carrier of (MultGroup E) \/ {(0. E)} by UNIROOTS:15;
then reconsider a = g as Element of E by XBOOLE_0:def 3;
set Fa = FAdj (F,{a});
C: the carrier of (FAdj (F,{a})) c= the carrier of E by EC_PF_1:def 1;
the carrier of E c= the carrier of (FAdj (F,{a}))

proof

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

let o be object ; :: thesis: ( o in the carrier of E implies b₁ in the carrier of (FAdj (F,{a})) )
assume o in the carrier of E ; :: thesis: b₁ in the carrier of (FAdj (F,{a}))
then reconsider b = o as Element of E ;

per cases ( b = 0. E or b <> 0. E ) ;

suppose b = 0. E ; :: thesis: b₁ in the carrier of (FAdj (F,{a}))

then b = 0. (FAdj (F,{a})) by FIELD_6:def 6;
hence o in the carrier of (FAdj (F,{a})) ; :: thesis: verum

end;

suppose b <> 0. E ; :: thesis: b₁ in the carrier of (FAdj (F,{a}))

then not b in {(0. E)} by TARSKI:def 1;
then reconsider h = b as Element of (MultGroup E) by B, XBOOLE_0:def 3;
consider n being Nat such that
E: h = g |^ n by A;
a |^ n = g |^ n by FIELD_15:10;
hence o in the carrier of (FAdj (F,{a})) by E, ThA; :: thesis: verum

end;

end;

end;

hence the carrier of E c= the carrier of (FAdj (F,{a})) ; :: thesis: verum

end;

then D: the carrier of E = the carrier of (FAdj (F,{a})) by C, XBOOLE_0:def 10;
( the carrier of (FAdj (F,{a})) c= the carrier of E & the addF of (FAdj (F,{a})) = the addF of E || the carrier of (FAdj (F,{a})) & the multF of (FAdj (F,{a})) = the multF of E || the carrier of (FAdj (F,{a})) & 1. (FAdj (F,{a})) = 1. E & 0. (FAdj (F,{a})) = 0. E ) by EC_PF_1:def 1;
hence E is F -simple by D, FIELD_7:def 1, FIELD_14:def 7; :: thesis: verum