let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F st K is F -algebraic holds
( K is E -algebraic & E is F -algebraic )
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F st K is F -algebraic holds
( K is E -algebraic & E is F -algebraic )
let K be E -extending FieldExtension of F; :: thesis: ( K is F -algebraic implies ( K is E -algebraic & E is F -algebraic ) )
H0: ( E is Subring of K & F is Subring of E ) by FIELD_4:def 1;
then H1: 0. K = 0. E by C0SP1:def 3;
assume AS: K is F -algebraic ; :: thesis: ( K is E -algebraic & E is F -algebraic )

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

let a be Element of K; :: thesis: a is E -algebraic
consider p being non zero Polynomial of F such that
A: Ext_eval (p,a) = 0. K by AS, FIELD_6:43;
reconsider p1 = p as Polynomial of E by H0, FIELD_4:9;
( 0_. E = 0_. F & p <> 0_. F ) by FIELD_4:12;
then reconsider p1 = p1 as non zero Polynomial of E by UPROOTS:def 5;
( p is Element of the carrier of (Polynom-Ring F) & p1 is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
then Ext_eval (p1,a) = Ext_eval (p,a) by lemma7b
.= 0. E by A, H0, C0SP1:def 3 ;
hence a is E -algebraic by H1, FIELD_6:43; :: thesis: verum

end;

hence K is E -algebraic ; :: thesis: E is F -algebraic

now :: thesis: for a being Element of E holds a is F -algebraic

let a be Element of E; :: thesis: a is F -algebraic
consider p being non zero Polynomial of F such that
A: Ext_eval (p,(@ (a,K))) = 0. K by AS, FIELD_6:43;
p is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
then Ext_eval (p,a) = Ext_eval (p,(@ (a,K))) by FIELD_6:11
.= 0. E by A, H0, C0SP1:def 3 ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

hence E is F -algebraic ; :: thesis: verum