let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
a is F -algebraic
let E be FieldExtension of F; :: thesis: for a being Element of E st a ^2 in F holds
a is F -algebraic
let a be Element of E; :: thesis: ( a ^2 in F implies a is F -algebraic )
assume a ^2 in F ; :: thesis: a is F -algebraic
then reconsider b = a ^2 as Element of F ;
Ext_eval ((X^2- b),a) = 0. E by lemBas00;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum