let E be F -finite FieldExtension of F; :: thesis: E is F -simple
consider T being finite F -algebraic Subset of E such that
A: E == FAdj (F,T) by FIELD_7:37;
defpred S₁[ Nat] means for E being F -finite FieldExtension of F
for T being finite F -algebraic Subset of E st card T = F & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T);
I: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume B0: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
( k <= 2 implies not not k = 0 & ... & not k = 2 ) ;

per cases then ( k = 0 or k = 1 or k = 2 or k > 2 ) ;

suppose B1: k = 0 ; :: thesis: S₁[k]

now :: thesis: for E being F -finite FieldExtension of F
for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)

let E be F -finite FieldExtension of F; :: thesis: for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
let T be finite F -algebraic Subset of E; :: thesis: ( card T = k & E == FAdj (F,T) implies ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) )
assume ( card T = k & E == FAdj (F,T) ) ; :: thesis: ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
then T c= the carrier of F by B1;
then B2: FAdj (F,T) == F by FIELD_7:3;
reconsider F1 = F as FieldExtension of F by FIELD_4:6;
set a = the F -algebraic Element of F1;
F is Subfield of E by FIELD_4:7;
then the carrier of F c= the carrier of E by EC_PF_1:def 1;
then reconsider a1 = the F -algebraic Element of F1 as Element of E ;
B3: FAdj (F,{a1}) = FAdj (F,{ the F -algebraic Element of F1}) by FIELD_10:9;
FAdj (F,{ the F -algebraic Element of F1}) == F by FIELD_7:3;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by B2, B3; :: thesis: verum

end;

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

end;

suppose B1: k = 1 ; :: thesis: S₁[k]

now :: thesis: for E being F -finite FieldExtension of F
for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)

let E be F -finite FieldExtension of F; :: thesis: for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
let T be finite F -algebraic Subset of E; :: thesis: ( card T = k & E == FAdj (F,T) implies ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) )
assume ( card T = k & E == FAdj (F,T) ) ; :: thesis: ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
then consider a being object such that
B2: T = {a} by B1, CARD_2:42;
a in T by B2, TARSKI:def 1;
then reconsider a1 = a as Element of E ;
FAdj (F,{a1}) = FAdj (F,T) by B2;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) ; :: thesis: verum

end;

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

end;

suppose B1: k = 2 ; :: thesis: S₁[k]

now :: thesis: for E being F -finite FieldExtension of F
for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)

let E be F -finite FieldExtension of F; :: thesis: for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
let T be finite F -algebraic Subset of E; :: thesis: ( card T = k & E == FAdj (F,T) implies ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) )
assume ( card T = k & E == FAdj (F,T) ) ; :: thesis: ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
then consider a, b being object such that
B2: ( a <> b & T = {a,b} ) by B1, CARD_2:60;
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
then reconsider a = a, b = b as Element of E by B2;
consider x being Element of F such that
B3: FAdj (F,{a,b}) = FAdj (F,{(a + ((@ (x,E)) * b))}) by simpA;
thus ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by B3, B2; :: thesis: verum

end;

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

end;

suppose B1: k > 2 ; :: thesis: S₁[k]

now :: thesis: for E being F -finite FieldExtension of F
for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)

let E be F -finite FieldExtension of F; :: thesis: for T being finite F -algebraic Subset of E st card T = k & E == FAdj (F,T) holds
ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
let T be finite F -algebraic Subset of E; :: thesis: ( card T = k & E == FAdj (F,T) implies ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) )
assume B2: ( card T = k & E == FAdj (F,T) ) ; :: thesis: ex p being Element of E st FAdj (F,{p}) = FAdj (F,T)
set a = the Element of T;
( T <> {} & T c= the carrier of E ) by B1, B2;
then reconsider a = the Element of T as Element of E ;
reconsider T1 = T \ {a} as finite F -algebraic Subset of E ;
reconsider k1 = k - 1 as Nat by B1;

now :: thesis: for o being object st o in {a} holds
o in T

let o be object ; :: thesis: ( o in {a} implies o in T )
assume o in {a} ; :: thesis: o in T
then ( o = a & T <> {} ) by B1, B2, TARSKI:def 1;
hence o in T ; :: thesis: verum

end;

then {a} c= T ;
then B6: T = T \/ {a} by XBOOLE_1:12
.= T1 \/ {a} by XBOOLE_1:39 ;
a in {a} by TARSKI:def 1;
then not a in T1 by XBOOLE_0:def 5;
then B9: card T = (card T1) + 1 by B6, CARD_2:41;
set E1 = FAdj (F,T1);
reconsider T2 = T1 as finite F -algebraic Subset of (FAdj (F,T1)) by FIELD_6:35;
B11: E is FAdj (F,T1) -extending by FIELD_4:7;
then B10: FAdj (F,T2) = FAdj (F,T1) by FIELD_13:19;
then consider q1 being Element of (FAdj (F,T1)) such that
B8: FAdj (F,{q1}) = FAdj (F,T2) by B0, B2, B9, NAT_1:19;
the carrier of (FAdj (F,T1)) c= the carrier of E by EC_PF_1:def 1;
then reconsider q = q1 as Element of E ;
consider x being Element of F such that
B5: FAdj (F,{q,a}) = FAdj (F,{(q + ((@ (x,E)) * a))}) by simpA;
FAdj (F,T) = FAdj (F,({q} \/ {a})) by B6, B8, B10, B11, FIELD_13:19, simp1
.= FAdj (F,{q,a}) by ENUMSET1:1 ;
hence ex p being Element of E st FAdj (F,{p}) = FAdj (F,T) by B5; :: thesis: verum

end;

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

end;

end;

end;

J: for n being Nat holds S₁[n] from NAT_1:sch 4(I);
consider n being Nat such that
K: card T = n ;
consider p being Element of E such that
L: FAdj (F,{p}) = FAdj (F,T) by A, J, K;
thus E is F -simple by A, L; :: thesis: verum