let F1, F2 be Field; :: thesis: for E being F1 -algebraic FieldExtension of F1 st F1 == F2 holds
E is F2 -algebraic FieldExtension of F2
let E be F1 -algebraic FieldExtension of F1; :: thesis: ( F1 == F2 implies E is F2 -algebraic FieldExtension of F2 )
assume AS: F1 == F2 ; :: thesis: E is F2 -algebraic FieldExtension of F2
then reconsider E3 = E as FieldExtension of F2 by lift9;

now :: thesis: for a being Element of E3 holds a is F2 -algebraic

let a be Element of E3; :: thesis: a is F2 -algebraic
reconsider a1 = a as Element of E ;
consider p being non zero Polynomial of F1 such that
B: Ext_eval (p,a1) = 0. E by FIELD_6:43;
reconsider p1 = p as non zero Polynomial of F2 by AS, lift6;
Ext_eval (p1,a1) = 0. E3 by B, AS, lift7;
hence a is F2 -algebraic by FIELD_6:43; :: thesis: verum

end;

hence E is F2 -algebraic FieldExtension of F2 by FIELD_7:def 11; :: thesis: verum