let F be Field; :: thesis: for K being FieldExtension of F
for E being b₁ -extending FieldExtension of F st E is F -separable holds
( E is K -separable & K is F -separable )
let K be FieldExtension of F; :: thesis: for E being K -extending FieldExtension of F st E is F -separable holds
( E is K -separable & K is F -separable )
let E be K -extending FieldExtension of F; :: thesis: ( E is F -separable implies ( E is K -separable & K is F -separable ) )
assume AS: E is F -separable ; :: thesis: ( E is K -separable & K is F -separable )
then A: ( E is K -algebraic & K is F -algebraic ) by FIELD_7:40;

now :: thesis: for a being Element of E holds a is K -separable

let a be Element of E; :: thesis: a is K -separable
reconsider b = a as K -algebraic Element of E by AS;
reconsider c = a as F -algebraic Element of E by AS;
set f = MinPoly (c,F);
set g = MinPoly (b,K);
MinPoly (c,F) is Polynomial of K by FIELD_4:8;
then reconsider f1 = MinPoly (c,F) as Element of the carrier of (Polynom-Ring K) by POLYNOM3:def 10;
deg (MinPoly (c,F)) > 0 by RING_4:def 4;
then deg f1 > 0 by FIELD_4:20;
then reconsider f1 = MinPoly (c,F) as non constant Element of the carrier of (Polynom-Ring K) by RING_4:def 4;
K: f1 is separable by AS, YY;
0. E = Ext_eval ((MinPoly (c,F)),c) by FIELD_6:51
.= Ext_eval (f1,b) by FIELD_7:15 ;
then consider r being Polynomial of K such that
H: (MinPoly (b,K)) *' r = f1 by RING_4:1, FIELD_6:53;
( MinPoly (b,K) is non constant Element of the carrier of (Polynom-Ring K) & r is Element of the carrier of (Polynom-Ring K) ) by POLYNOM3:def 10;
then MinPoly (b,K) is separable by H, K, ThSepPR;
hence a is K -separable ; :: thesis: verum

end;

hence E is K -separable by AS, FIELD_7:40; :: thesis: K is F -separable

now :: thesis: for a being Element of K holds a is F -separable

let a be Element of K; :: thesis: a is F -separable
reconsider b = a as F -algebraic Element of K by A;
K is Subfield of E by FIELD_4:7;
then the carrier of K c= the carrier of E by EC_PF_1:def 1;
then reconsider c = b as F -algebraic Element of E by AS;
MinPoly (b,F) = MinPoly (c,F) by FIELD_10:10;
hence a is F -separable by AS; :: thesis: verum

end;

hence K is F -separable by AS, FIELD_7:40; :: thesis: verum